Specification language
t-language
I’m building t: a small specification language that turns one program and its contract into inputs for Dafny, Verus, SPARK, Frama-C, Lean 4, Rocq, and F*.
The actual wrong-var mutation is max(x, min(hi, x)). Recorded proof: Dafny 4.11.0; other backends are not replayed in the browser.
Choose x. The shaded interval is the permitted output range, 0 through 10. The markers use the same numerical axis.First evaluate min(10, x). An input above 10 is capped at 10; every other input is unchanged.Then evaluate max(0, min(10, x)). An input below zero becomes zero. The resulting value is the original program’s output.The engine’s wrong-var twin replaces lo with x in max(lo, …). That expression returns x, exposing the missing clamp on out-of-range inputs.
clamp.t + recorded proof ↗- Input: Choose x. The shaded interval is the permitted output range, 0 through 10. The markers use the same numerical axis.
- min: First evaluate min(10, x). An input above 10 is capped at 10; every other input is unchanged.
- max: Then evaluate max(0, min(10, x)). An input below zero becomes zero. The resulting value is the original program’s output.
- Twin: The engine’s wrong-var twin replaces lo with x in max(lo, …). That expression returns x, exposing the missing clamp on out-of-range inputs.
What I’m building
Write a typed program, its preconditions, and its postconditions once. The tool lowers that task into supported proof-system inputs and reports each checker’s result.
The “twin rule” checks a deliberately broken version too. A result only counts when the original is proved and a concrete failure of the twin is certified.
Read the code
A small example
This clamp task bounds its result and preserves inputs already inside the interval.
t 1
task clamp(x: int, lo: int, hi: int) returns (r: int)
requires lo <= hi
ensures lo <= r and r <= hi
ensures lo <= x and x <= hi ==> r == x
{
r := max(lo, min(hi, x));
}What a result means
A proof is about the written contract and its assumptions. Supported constructs differ between backends, and some share underlying solvers. The reports name refusals and missing coverage.
The engine previously lived under the t-proof-engine repository name. The current public repository is t-language. See its Research Use License before reusing it.