Proofs and specifications
Specifies a protocol or algorithm and checks it exhaustively or proves it, catching design bugs before code exists.
V1030 technique
2 of 256 scanned repositories run it (1%)
Sub-techniques
3
| ID | Name | Description |
|---|---|---|
V1030.001 | Model checking a design | Write a TLA+ spec and check invariants over all reachable states. |
V1030.002 | Verified code | Write code with pre- and post-conditions that a verifier proves (Dafny, Lean, Rocq). |
V1030.003 | Proof harnesses on real code | Bounded proofs over the production code itself (Kani). |
Craft it
- Specify the part where a bug is catastrophic and tests are weak: consensus, replication, locking.
- Check the spec in CI on every change to it.
- Link spec actions to code with comments or trace checking.
Reverse engineer it
Signs that a codebase already runs this technique, and where to read how it is configured.
- *.tla, *.dfy, *.lean or *.v files and a CI job that runs the checker.
- #[kani::proof] harnesses.
Where the scanned repositories configure it:
show_manual_release_cmd_test.vin 1 repositoriesv.vin 1 repositories
Detected by the scanner as: Proofs and specifications (design-level bugs in protocols and algorithms, checked against a specification.)
Open-source packages
5
- TLA+ tools tlaplus/tlaplus
- Dafny dafny-lang/dafny
- Lean 4 leanprover/lean4
- Rocq (Coq) rocq-prover/rocq
- Kani model-checking/kani
Tools seen in scans
by repositories that run them
Procedure examples
repositories that run it, most-starred first
| Repository | Tools | Runs in | Evidence |
|---|---|---|---|
| helix-editor/helix | coq |
tests/indent/v.v 2 file(s) |
|
| vlang/v | coq |
.github/show_manual_release_cmd_test.v 9829 file(s) |