AutoProof

AutoProof is an auto-active verifier for functional properties of the Eiffel programming language. It uses the Boogie verifier as a back-end.

To get started with AutoProof take a look at the AutoProof quick start guide.

A more systematic description of AutoProof is in the AutoProof tutorial.