Awesome Reviewers

Verification · 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).

How to build it

  1. Specify the part where a bug is catastrophic and tests are weak: consensus, replication, locking.
  2. Check the spec in CI on every change to it.
  3. Link spec actions to code with comments or trace checking.

Signals in a repository

  • *.tla, *.dfy, *.lean or *.v files and a CI job that runs the checker.
  • #[kani::proof] harnesses.