Verification · Formal · Symbolic execution
Bounded model checking
Unroll loops to a bound and check all paths (CBMC).
How to build it
- Write a harness that sets the inputs of one function to nondeterministic values.
- Set an unwinding bound for each loop and check that the bound is reached.
- Run the checker in CI with a time limit per harness.
Signals in a repository
- CBMC harness files or Kani proof functions in the source tree.
- CI steps that invoke cbmc or cargo kani.
- unwind or unwinding settings in harness or config files.
In practice
No scanned repository runs a tool for this check. The steps above are the only guidance.