AutoProof is an auto-active verifier for object-oriented programs written in the Eiffel programming language. It uses Boogie as a back-end.

This page documents AutoProof 2015: the version of AutoProof presented in the TACAS 2015 and FM 2015 papers listed below. AutoProof 2015 offers a stable set of features; it is made available here for future reference. Henceforth, we refer to AutoProof 2015 simply as AutoProof.

Try AutoProof online

You can use AutoProof on ComCom in your browser without downloading anything. AutoProof on Comcom is limited to single-class projects.

Download AutoProof

AutoProof is a component of the open-source Eiffel Verification Environment (EVE). To use all features of AutoProof you can download a pre-compiled version of EVE (see file INSTALL for the simple installation instructions).


Gallery of verified programs

A software repository collects a suite of benchmark problems implemented in Eiffel and verified with AutoProof. You can run verification online and see the results!


The following people took part in the AutoProof project:

AutoProof Source code

The source code of EVE (with AutoProof) is also available; it is distributed under GPL v. 2. AutoProof was written by Julian Tschannen and Nadia Polikarpova.