Specification and Formal Verification of the Aztec Governance Protocol
A detailed blogpost that summarizes our work on formal specification of Aztec Governance and showing its safety with inductive invariants...
In August 2025, Aztec Labs engaged Thomas Pani and me to formally specify and verify the new Aztec Governance Protocol – the core on-chain system that governs Aztec Network.
See a detailed write-up of our work in this technical blogpost and even more details in the report.
Over the course of five weeks, we reviewed every line of code in scope and developed a precise formal specification, verified automatically with Apalache. The result: scalable, massively parallel automated verification that explored the entire protocol state space to formally confirm correctness and uncover subtle, cross-contract issues that conventional audits or fuzzing can easily miss.
The team at Aztec Labs reviewed our findings and addressed all of them.
| 125 invariants specified across 10 contracts, 8 libraries, and 8 interfaces |
| 992 verification conditions checked in total |
| 72 physical cores / 368 GiB RAM, running for 321 CPU-days (≈ 2 weeks) |
| Findings: 5 Medium • 3 Low • 6 Info |
| Final complete verification run in 576 CPU-hours (≈ 1 calendar day) |
| Contract size: ~2 kLOC Solidity |
| Specification size: ~4 kLOC Quint (incl. traceability comments) |