- take the basic arithmetic operators:
| Description | Operation |
|---|---|
| Addition | x + y |
| Subtraction | x - y |
| Multiplication | x * y |
| Integer division | x // y |
| Exponentiation | x**y |
| Modulo | x % y |
- create an external entrypoint for each operator
- create invariants for all operators
- prove the correctness of the spec using Certora Prover
export CERTORAKEY=your_key- to run the tests:
certoraRun config.conf