| Abella |
Abella is an interactive theorem prover based on lambda-tree syntax.
|
| BEAGLE |
Beagle is an automated theorem prover for first-order logic with equality over linear … |
| Gappa |
Gappa is a tool intended to help verifying and formally proving properties on numerical programs … |
| Metis |
[ Not Maintained Since 2020 ] Metis is an automatic theorem prover for first order logic with … |
| MetiTarski |
MetiTarski is an automatic theorem prover based on a combination of resolution and a decision … |
| Princess |
Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted … |
| 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.
|