runtimeverification / runtimeverification/kontrol
Run KEVM on existing projects' test suite
@JuanCoRo is already working on this.
Since Sep 21, 2023.
- Dominant language
- Python
- Stars
- 122
- Forks
- 16
- PR merge metrics
- No merged PRs in 30d
Description
We should evaluate Kontrol against some existing test suite of a DeFi protocol. We should also conduct a “where are we at” review of KEVM to plan future work.
Also, we should run Kontrol on the bug in prb-math found by the Certora prover and presented at DSS (credit: @JuanCoRo):
- Blog post explaining the bug
- The mulDivSigned function where the bug was present
Another bug we should be able to detect is the overflow found using new ToB's fuzzer Medusa: https://twitter.com/transmissions11/status/1688601302371389440?s=20. We can also verify the equivalence between the original and optimized version: https://twitter.com/real_philogy/status/1688838433563623426.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.