vac:sc:codex:formal-verification_2024q4
Implementation of the first 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. Formal verification is an iterative process, however we’ve identified a handful of rules we’re committing to delivering by the end of this quarter.
Task List
Finish implementing current rules
- fully qualified name:
vac:sc:codex:formal-verification_2024q4:finish-current-rules - owner: r4bbit
- status: in progress (40%)
- start-date: 2024/10/14
- end-date: 2024/11/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