Technique · Formal

Proofs and specifications

Specifies a protocol or algorithm and checks it exhaustively or proves it, catching design bugs before code exists.

Sub-techniques

Model checking a design V1030.001

Write a TLA+ spec and check invariants over all reachable states.
Verified code V1030.002

Write code with pre- and post-conditions that a verifier proves (Dafny, Lean, Rocq).
Proof harnesses on real code V1030.003

Bounded proofs over the production code itself (Kani).