AutoProof is a verifier of object-oriented programs that uses Boogie as a back-end. AutoProof is an ongoing development of the Chair of Software Engineering at SIT, based on an earlier implementation at ETH Zurich.

AutoProof online

You can use AutoProof in your browser without downloading anything. This version is limited to single-class projects.

AutoProof as a GitHub action

You can make AutoProof action part of your GitHub project continuous development pipeline.

Docker image with AutoProof

You can pull a Docker image with a full-fledged Linux-based distribution of AutoProof.

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!


Current contributors

The following people are currently working on AutoProof (alphabetically):

Former contributors

The following people have initially developed AutoProof: