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:
  • status: not started
  • 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