Verification · Formal · Symbolic execution
Contract checking
Search for inputs that break a function's pre- and post-conditions (CrossHair).
How to build it
- Add type annotations and pre- and post-conditions to small pure functions.
- Run crosshair check on those modules with a time budget per function.
- Turn each counterexample into a unit test.
Signals in a repository
- crosshair configuration or check commands in CI or the Makefile.
- Contract decorators or assert statements that state pre- and post-conditions.
- Test cases named after counterexamples found by the checker.
In practice
No scanned repository runs a tool for this check. The steps above are the only guidance.