Program Prover
| Tool | Description |
|---|---|
| Gillian | Gillian is a multi-language analysis platform supporting, e.g., verification and symbolic testing. … |
| Aeneas | Aeneas (pronunced [Ay-nay-as]) is a verification toolchain for Rust programs. |
| Creusot | Creusot is a deductive verifier for Rust code. |
| Dafny | Dafny is a verification-aware programming language that has native support for recording … |