Formal Methods Tools

Program Proof Tools

This page lists all of the program proof tools on this site in alphabetical order. Click a tool name in the first column to view tool details. Click a colorful item in the second column to view all the tools for which that term applies. Item colors mean nothing and are intended to make it easy to skim the page. Colors are generated by hashing each term’s name and converting it to RGB color values.

Tool Applications Licenses
Aeneas Program Prover Rust Verifier Apache-2.0
Creusot Program Prover Rust Verifier LGPLv2.1
Dafny Program Prover MIT
Gillian Program Prover BSD-3-Clause
Kani Model Checker Rust Verifier Apache-2.0 MIT
Loom Rust Verifier MIT
Loom Rust Verifier MIT
Miri Rust Verifier Apache-2.0 MIT
Rust Verifier Mozilla-2.0
Verus Rust Verifier MIT
Red dot indicates tool has not been updated or maintained recently