issues
search
NethermindEth
/
horus-checker
Horus, a formal verification tool for StarkNet smart contracts.
https://nethermind.io/horus/
Other
71
stars
7
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Update `fourmolu` to set column limit
#199
langfield
opened
1 year ago
0
Don't verify `@external`-generated wrapper functions
#198
langfield
opened
1 year ago
1
`horus-compile` raises a `typeguard` runtime error on Python 3.9
#197
langfield
opened
1 year ago
1
Don't verify commits anymore
#196
langfield
closed
1 year ago
0
Add missing range check bound to `assert_nn_le()` spec
#195
Julek
opened
1 year ago
0
Remove explicit import lists for qualified imports
#194
langfield
opened
1 year ago
0
Add mathsat installation to Github actions workflow
#193
langfield
closed
1 year ago
0
Add `README.md` section on details of `CairoSemanticsL`
#192
langfield
closed
1 year ago
0
Flatten return tuples of storage variables
#191
langfield
opened
1 year ago
1
Refactor `Module.hs` DFS logic
#190
langfield
opened
1 year ago
3
Fix improper handling of post with a reference to storage
#189
langfield
closed
1 year ago
0
Remove distinction between rich and plain specs
#188
langfield
closed
1 year ago
0
Remove checkpoints, check preconditions in separate modules, document `CairoSemantics.hs`
#187
langfield
closed
1 year ago
0
Fix improper handling of post with a reference to storage
#186
langfield
closed
1 year ago
0
add check for repeated storage_updates up to syntactic equality of ar…
#185
Ferinko
closed
1 year ago
1
fix improper handling of post with a reference to storage
#184
Ferinko
closed
1 year ago
1
implement comment injections
#183
Ferinko
opened
1 year ago
0
Verified commits check
#182
ElijahVlasov
closed
1 year ago
0
Ferinko/dry rebase
#181
Ferinko
closed
1 year ago
0
Filtered master for ferinko
#180
langfield
closed
1 year ago
0
Install horus-compile from public PyPI
#179
ElijahVlasov
closed
1 year ago
0
Ferinko/checkpoint gone
#178
Ferinko
closed
1 year ago
0
How to use loop invariants
#177
Leonard-Pat
opened
1 year ago
7
Change branch identifiers from `:::T/F` to `:::1/2`
#176
langfield
closed
1 year ago
0
Fix combination of subgoals
#175
aemartinez
closed
1 year ago
3
Are `@storage_update` annotations supported in namespaces?
#174
Leonard-Pat
closed
1 year ago
1
Checking storage update of external contract
#173
Leonard-Pat
closed
1 year ago
3
Filter non-precondition asserts
#172
langfield
closed
1 year ago
1
Fix: typos
#171
omahs
closed
1 year ago
0
Something is wrong with the implications in queries
#170
langfield
opened
1 year ago
2
Possibility to see the counter-example generated by the SMT solver
#169
acmLL
opened
1 year ago
10
Don't verify `@external`-generated wrapper functions
#168
Ferinko
closed
1 year ago
0
Contradictory premises
#167
acmLL
closed
1 year ago
2
Cairo semantics comments
#166
langfield
closed
1 year ago
0
fix improper handling of 'and' in pre
#165
Ferinko
closed
1 year ago
1
MakerDAO `frob()` verification efforts
#164
langfield
closed
1 year ago
0
Strange syntax error from `horus-compile` for non-imported function in separate module
#163
langfield
closed
1 year ago
1
Julek/math sat fix
#162
Julek
closed
1 year ago
3
The semantics of operator `/` in assertions is not the proper `felt` semantics
#161
aemartinez
opened
1 year ago
2
Update `toy_amm.cairo` example for inlining
#160
langfield
closed
1 year ago
1
Don't mark functions in `stdSpecsList` as user-annotated
#159
langfield
closed
1 year ago
1
Docs: add mention to json specification file where missing.
#158
aemartinez
closed
1 year ago
0
Example usage from `README.md` is missing `spec.json` argument to `horus-check`
#157
langfield
closed
1 year ago
0
Add FAQ about commenting-out annotations
#156
langfield
closed
1 year ago
1
Add FAQ about account contracts
#155
langfield
closed
1 year ago
0
Add label to `@invariant` example in `README.md`
#154
langfield
closed
1 year ago
0
Test cases for `@assert` notation
#153
langfield
opened
1 year ago
0
Detect contradictory premises
#152
langfield
closed
1 year ago
0
Namespaces cause unpredictable change in behaviour
#151
Ferinko
closed
1 year ago
2
Revertable function
#150
acmLL
opened
1 year ago
7
Next