Formal Methods Tools

At a Glance

Applications Theorem Prover
Developers ConsenSys
Interfaces CLI
Licenses Apache-2.0
Maintenance Actively Maintained

Description

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.