vac:sc:codex:2025q1-formal-verification
Finishing the implementation of all agreed upon formal verification rules for the Codex marketplace contracts.
Description
We’re collaborating with the Codex team and the Certora team to formally verify the marketplace contracts for the Codex network. We’ve already implemented many rules in the previous iteration, however we left some rules unfinished that we’re committing to finish in this quarter.
Task List
Finish implementing current rules
- fully qualified name:
2025q1-formal-verification:finish-current-rules - owner: r4bbit
- status: not started
- start-date: 2025/01/01
- end-date: 2025/03/31
Description
There’s a few rules ideas we’ve drafted out with the Certora team. For most of them we’ve created dedicated issues on GitHub.
The task is to finish these together with Certora.
Deliverables
- Certora spec files containing rules listed in the GitHub issues