| Aeneas |
Aeneas (pronunced [Ay-nay-as]) is a verification toolchain for Rust programs.
|
| Abella |
Abella is an interactive theorem prover based on lambda-tree syntax.
|
| Gappa |
Gappa is a tool intended to help verifying and formally proving properties on numerical programs … |
| MetiTarski |
MetiTarski is an automatic theorem prover based on a combination of resolution and a decision … |
| Profound |
[ Not Maintained Since 2011 ] Profound is an experiment in subformula linking as an interaction … |
| SPASS |
[ Closed-Source Tool ] SPASS: An Automated Theorem Prover for First-Order Logic with Equality … |
| Why3 |
Why3 is a platform for deductive program verification.
|