Verification · Formal · Proofs and specifications
Proof harnesses on real code
Bounded proofs over the production code itself (Kani).
How to build it
- Write a proof harness next to the production function, with symbolic inputs and assertions.
- Set the bounds for loops and input size and record them in the harness.
- Run the proof tool in CI on the crate or file that contains the harness.
Signals in a repository
- #[kani::proof] functions in Rust source files.
- A cargo kani step in a workflow.
- CBMC harness files or Makefile targets that run cbmc on production sources.
In practice
No scanned repository runs a tool for this check. The steps above are the only guidance.