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.
For some unknown reason, this is failing:
define nat(int r) is: r >= 0 assert: forall(int i): nat(0)