Principle 7 of 10
Formal Verifiability
The consensus protocol must be formally specified and machine-verified.
Every major distributed systems failure in blockchain history — from the DAO hack to bridge exploits — involved behaviour that was unspecified or incorrectly specified in natural language. TLA+ and Lean 4 are the current standards for formal protocol specification. The obstacle is not capability — it is engineering investment that most projects decline.
Scoring Rubric
| Score | Criteria |
|---|---|
| 7–10 | TLA+ spec published and model-checked; cryptographic properties proven in Lean 4 or Coq; peer-reviewed. |
| 4–6 | Informal specification with test suite; or TLA+ spec without model checking. |
| 0–3 | Protocol specified only in natural language or reference implementation. |
Data Sources
- Published TLA+/Lean 4 specifications
- Peer review letters
- Model checking results