A compiler that refuses a contract that says too little

This article was written with the help of an AI assistant (Claude), like the language it describes, which was built with Claude Code. I checked every figure against the repository and I take responsibility for the content. It follows Green proofs, empty promises.

A green proof that proves little

In my previous article I asked a small model to write verified Dafny. The proofs were green. But 5 of the 8 contracts barely constrained the result: a length, a format, a shape. One of those methods was wrong, and the proof did not notice.

A verifier proves what it is asked to prove. If the same agent writes the code and its contract, it can ask for exactly as much as it manages to prove. Checking the proof is not enough; the question is whether the contract says enough.

The idea

I built a small language, Quod, to try one rule: the compiler asks whether two different results could both satisfy the contract. If so, it refuses the program and shows you the two results.

fn clamp(x: int, lo: int, hi: int) -> int
  requires lo <= hi
  ensures lo <= result && result <= hi
{
  if x < lo { lo } else if x > hi { hi } else { x }
}

$ quod check clamp_weak.quod
error: in clamp: the contract accepts two different results for the same input:
add ensures clauses until only the intended result is allowed, or declare the freedom with 'loose'
    witness: x = 0, lo = 0, hi = 1, result_a = 1, result_b = 0

For x = 0 in [0, 1], both 0 (the right answer) and 1 satisfy the contract. This is a contract that a verifier would accept with a green proof, because clamp does stay within [lo, hi]. Here is what it was missing:

  ensures lo <= result && result <= hi
  ensures lo <= x && x <= hi ==> result == x
  ensures x < lo ==> result == lo
  ensures x > hi ==> result == hi

verified: 4 proof obligation(s) proved; 1 of 1 contract(s) determine their result; contracts: 1 by properties

Two things keep this from being a trick:

• You cannot cheat by copying the body. A contract that just restates the code is complete, so the compiler reports the style of every contract (properties, model, restated, missing) and warns when it is only a restatement. In my first experiments, 4 of 6 agent-written contracts defined the result with a second implementation, and this is what the warning is for.
• Freedom can be declared, but it is watched. If several results are really acceptable (any index of a duplicate in a binary search), you write loose (a, b) => ... with what the two results must have in common, and the compiler shows an example. A loose that holds for any two results is reported as proving nothing, and can be refused outright.

Everything else is classic: contracts, loop invariants and termination are proved with Z3, which ships in the release package. The check itself is a satisfiability question: do the preconditions and two different results, both allowed by the postconditions, have a solution? When the solver cannot decide, the check only warns, so "refuses" means "refuses when it can tell".

What exists

• Pure functions with contracts, lemmas, modules, strings, bounded integers (i32, i64), structs, enums, match and generics.
• A Python backend, and a C# backend (C# 7.3, so it also targets .NET Framework 4.7.2). The C# for clamp is what you would write:

public static long Clamp(long x, long lo, long hi)
{
    if (!(lo <= hi)) throw new ArgumentException("clamp: requires lo <= hi");
    return _quod_f_clamp(x, lo, hi);
}

Quod's int is a long computed in checked: an overflow throws rather than returns a wrong result. i32 and i64 have their bounds proved. I have not measured the speed of the generated C#.

• An MCP server (quod mcp), so that an agent can write, check and correct in a loop, and a NuGet package (attached to the releases, not on nuget.org) that generates the C# at build time. z3 comes in the release archive, so a CI job only downloads it.

Today it is limited to pure functions: no input or output, no maps or sets, yet. Input and output are planned, as capabilities (a function touches the console, files or the network only through a capability it receives, so the contract still says what it may do), together with maps and sets: it is the next item of the roadmap. There are no classes and none are planned; structs, enums and generics cover the data. You call a Quod function from Python or C#.

What I measured

• Agents can write programs of a useful size in it. Two models wrote billing engines of about 300 lines over three modules, from the language reference alone. All 24 runs verified and agreed with an oracle. The rules, the oracle and the compiler have one author, so this shows the tool works on one kind of program; it does not show that the test was hard.
• With a capable model, the rule did not change the number of complete contracts. I measured no gain. My reading: a capable model already writes contracts that fix the result, so the rule works as a guardrail for the reviewer, not as a teacher for the model.
• Against Dafny, my soundness measure could not tell the two apart on 72 held-out runs (four setups, six tasks, a small model). I can claim a different design and a different workflow, not better soundness.
• A small model is not helped by the message. A 14B local model got 0 of 18 accepted, mostly stuck on syntax it had learned from Dafny. The error for a missing contract does not teach it to write one.
• A complete contract can still be the wrong one. One run produced ensures len(result) == 0 over return []. The rule asks whether the contract fixes the result, not whether it is the result you meant. A human still has to read the contracts, which is why the compiler lists the ones to review.

What the proofs are worth

Several adversarial reviews, by a language model told to attack the compiler with programs that can be replayed, found real problems, and I fixed all of them. Two kinds:

• False proofs: a length axiom that was too strong, a loop helper called without its precondition, and z3 answering unsat to a satisfiable question after an interrupted check. I saw the last one as wrongly refused builds, about 1 in 300 on one family of files (release notes); a proof rests on the same answer, so I treated it as a risk to proofs and looked for false proofs afterwards, without finding one.
• Generated code that contradicted a proof: a Python variable that hid a class, and, in C#, two modules whose names differ only by case, a_b and aB, that became one class.

The last review, of 0.4.0, found no false proof and no such contradiction in the default build. I do not claim none is left. One known limit: with a time budget (--budget), which obligations are cut can depend on the speed of the machine.

Where it stands against what I know

Completeness of generated specifications has been studied: Lahiri (2024) scored LLM-generated Dafny postconditions by whether they reject mutated outputs, and VeriEquivBench (2025) proves specifications equivalent to the code (I have read only part of that paper). Both measure after the fact. The experiment here is to put the question in the compiler, where the agent reads the answer while it writes.

Try it, and tell me where it was hard

Almost nobody but me has used Quod. That is the real gap, more than any missing feature.

There is a 30-minute path: download a release (Windows, Linux or macOS; z3 is inside), check an example, read the error of the weak contract, generate Python and C#, and write a small function of your own. Then tell me where you got stuck, using this short form. "I gave up at step 2, because..." is a perfectly good report.

If you read C#, I am especially interested in the generated code. I have written C# for more than twenty years and judge it by reading it, and I would like to know whether it looks normal to someone else.

Repository: https://github.com/quod-lang/quod