Green proofs, empty promises: when AI agents write their own specifications
Description and use
LLM-generated code can pass Dafny verification yet still contain bugs because the specifications are incomplete. The article presents a method to detect such empty contracts by proving uniqueness of postconditions and generating witnesses where the contract accepts multiple outputs.
Problem
AI coding agents can produce formally verified code that still contains bugs because the specifications they write are incomplete.
Outcome
Out of 24 agent-written Dafny contracts, 15 had unique postconditions, 6 were underspecified with witnesses, and 3 were inconclusive. The Haiku model produced one escaped bug in both Python and Dafny arms, but the Dafny bug was due to an underspecified contract.
Workflow
- 1. Generate Dafny code and specifications with an LLM.
- 2. Run dafny verify to ensure the verifier accepts the solution.
- 3. For each method, ask Dafny to prove that two different results satisfy the postcondition for the same input.
- 4. If the proof fails, construct concrete inputs and run the method to obtain actual outputs.
- 5. Build neighboring outputs and ask Dafny to prove the contract accepts both.
- 6. If both proofs succeed, the contract is underspecified; record the witness.
- 7. Aggregate results to assess the prevalence of underspecification.
Evidence
A verifier only guarantees what you ask it to.
For a method with precondition R and postcondition E, ask: Can two different results both satisfy E, for the same valid input?
The trick: take small concrete inputs, run the method to get its actual answer a, build neighbouring answers b, and ask Dafny to prove that the contract accepts both a and b on those concrete values.
The six witnesses: ...
- Record date: 2026-10-21T08:56:17.458Z