Python's Deal library provides contracts and a small portable formal proofs area of the codebase.
Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered.
It just works surprisingly well for incrementally building up provable code properties.
Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered.
It just works surprisingly well for incrementally building up provable code properties.