Qualification Requirements

Our judges will assess the specification based on the following criteria: Soundness - the spec should correctly describe the desired behaviors of the code. Abstraction - a good spec should describe high-level properties of the code and not just “unit-tests.” Security coverage - a specification that can prevent bugs in different components and of different types would be rated higher. Correctness - the specification should be a valid input to the Certora Prover, and we can trigger a run with it. Note - please send your specifications even if the Prover halts on your runs or finds violations! Submission A link to your prover runs. Adding comments to your specification will increase your chances of earning a reward. A link to your project’s repository, that should contain documentation about your project