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.…