One language, seven targets
Write a program and its specification in t. The engine lowers them to Dafny, Verus, SPARK, Frama-C, Lean, Rocq, and F*. Unsupported constructs are reported explicitly.
01 / Formal verification
t-proof-engine
SPECIFY · PROVE · REFUTE
Write it once.
Check it seven ways.
A specification language that checks programs across seven proof systems, and challenges every result with a deliberately broken twin.
View repository7proof systems
23UVa problems in the published table
179,549judge-output lines matched
From the public project record reviewed 08 October 2026. View source and measurement context ↗
Inside the project
Built around
the details.
A proof has to distinguish right from wrong
A result counts only when the original program is proved and a deliberately broken version is refuted at a concrete input. The second check helps expose specifications that are too weak.
A showcase you can trace
The published UVa collection pairs proofs with exact comparisons against stored uDebug outputs. Every row identifies which systems succeeded and what the specification actually states.
What the results mean
The published table contains 23 problems proved in at least one system; 3 pass all seven. A proof establishes the written specification under its preconditions. Some specifications encode mathematical models whose relationship to the original story is not itself proved. Input/output adapters and generated execution are tested, not proved. Several front ends also share underlying solvers.
Follow the evidence