DEV Community: Malek AIT OUARET

Green proofs, empty promises: when AI agents write their own specifications

Malek AIT OUARET — Wed, 21 Oct 2026 07:44:35 +0000

I asked AI coding agents to write formally verified code. Every solution passed the
verifier. Then I checked what the proofs actually promised.

For the smaller model, 5 of 8 specifications barely said anything. One of the
methods was wrong, and its proof was green.

This post is about that gap, a cheap way to detect it, and a small open-source tool that does it
for any Dafny file.

The experiment

I'm designing a programming language meant to be written by agents and checked by machines
(more on that at the end). Before designing anything, I wanted data: when an agent has to prove
its code, do fewer bugs slip through?

The setup (VerifBench):

8 short algorithmic tasks chosen because LLMs classically stumble on them: Gregorian day counting (leap centuries), strict UTF-8 validation (overlongs, surrogates), glob matching with escapes, an LRU cache, a lexicographically smallest topological sort, text justification, big-number addition (borrows, -0), Unix path normalization.
Same natural-language spec, two arms: plain Python (the agent may run its own tests), or Dafny, where the agent must write requires / ensures / invariants and get dafny verify to pass. Cheats like assume or {:verify false} are detected.
Claude Code as the agent, two models: claude-opus-5-5 and claude-haiku-4-5.
About 500 hidden tests per task, compared with an oracle. The Dafny code is compiled to Python and goes through exactly the same tests.

The key metric is the escaped bug: a solution the agent would ship (and, in Dafny, that
verifies) which still fails a hidden test.

The results look reassuring...

Model / arm	Escaped bugs	Cost per task*	Time per task
Opus / Python	0 / 8	$0.14	17 s
Opus / Dafny	0 / 8	$0.22	46 s
Haiku / Python	1 / 8	$0.15	106 s
Haiku / Dafny	1 / 8	$0.45	255 s

* API-equivalent estimate reported by the agent. One trial per cell: signals, not statistics.

Opus solved everything, with or without proofs. Haiku let one bug through in each arm. Proof
looks like it costs 1.5–3× more and buys... nothing here?

...until you read the Haiku Dafny bug

The escaped Dafny bug was in the LRU cache. The method verified. Here is its signature
(preconditions abridged) and its entire postcondition:

method lru_cache(capacity: int, ops: seq<(int, int, int)>) returns (out: seq<int>)
  requires capacity >= 1
  ensures |out| == CountGets(ops, |ops|)

The output has the right length. Nothing says which values a get returns. The code evicted
an entry every time a new key was inserted, whether the cache was full or not, and Dafny was
perfectly happy, because nothing in the contract forbade it.

A verifier only guarantees what you ask it to. And when the agent writes both the code and
the specification, it can, without any malice, ask for exactly as much as it manages to prove.

So I went back and checked all 24 Dafny contracts.

A simple question to ask a specification

For a method with precondition R and postcondition E, ask:

Can two different results both satisfy E, for the same valid input?

If the contract is complete, the answer is no:

∀ x, a, b :  R(x) ∧ E(x, a) ∧ E(x, b)  ⇒  a == b

This is a question about the contract only, not the code. And Dafny can answer it: generate
a lemma with exactly that statement and ask Dafny to prove it, with no hints.

ghost predicate Post(capacity: int, ops: seq<(int,int,int)>, out: seq<int>)
  requires capacity >= 1
{ |out| == CountGets(ops, |ops|) }

lemma Uniq(capacity: int, ops: seq<(int,int,int)>, a: seq<int>, b: seq<int>)
  requires capacity >= 1 && Post(capacity, ops, a) && Post(capacity, ops, b)
  ensures a == b
{}

When the proof goes through, the contract determines the result. When it fails, that may mean
the contract is incomplete... or just that the uniqueness proof is hard (it often needs
induction). To tell the two apart, you need a witness.

Finding witnesses

The trick: take small concrete inputs, run the method to get its actual answer a, build
neighbouring answers b (a changed digit, a dropped element, an emptied list...), and ask Dafny
to prove that the contract accepts both a and b on those concrete values.

If both proofs go through, you have a certain witness: no sampling, no guessing. Results on the
24 agent-written contracts:

Verdict	Count
Uniqueness proved	15
Underspecified, with a witness	6
Inconclusive	3

The six witnesses:

Method	Input	Two results the contract accepts
`add_big` (Haiku)	`"0" + "0"`	`"0"` and `"1"`
`topo_sort` (Haiku)	1 node, no edge	`[0]` and `[]`
`normalize_path` (Haiku)	`""`	`"."` and `".x"`
`justify` (Haiku)	`["a"]`, width 2	`["a "]` and `[]`
`lru_cache` (Haiku)	two `get`s on an empty cache	`[-1, -1]` and `[0, -1]`
`binary_search`	`[1, 1]`, target 1	`1` and `0`

Read them as sentences and they speak for themselves: according to its proved contract, the
addition is allowed to say 0 + 0 = 1. The topological sort may return nothing for a graph with
no edge. The path normalizer may return any non-empty string.

The last one, binary_search, is legitimately free: with duplicates, any index of the target
is a correct answer. A witness doesn't mean "bug"; it means "the contract allows a choice", and
someone should decide whether that choice is intended.

The striking part: four of Haiku's five near-empty contracts sat on correct code. The tests
passed, the proofs were green, and the proofs guaranteed almost nothing. Without this check,
"verified" on those methods was pure decoration.

And the three inconclusive ones? I read them: their contracts are complete (merging intervals
into a canonical union, run-length encoding, canonical decimal strings), but proving uniqueness
needs induction that the solver won't find alone. No witness was found for any of them, so the
tool never reported them as underspecified. Clean separation, on this small sample.

Opus, for the record, wrote contracts that were proved unique in 7 of 8 hard tasks, including a
full lexicographic-minimality specification for the topological sort.

The tool: dafny-complete

I turned this into a standalone checker that works on any .dfy file:

pipx install "git+https://github.com/quod-lang/quod#subdirectory=tools/dafny-complete"
dafny-complete my_file.dfy

  [OK]    Abs      line 11    the contract determines a unique result
  [UNDER] WeakAbs  line 19    the contract accepts two different results
                    input  : x=0
                    y = 0   (what the method returns)
                    y = 1   (also satisfies every ensures)

It runs four Dafny passes over the whole file (uniqueness lemmas, valid small inputs proved
against the preconditions, actual execution of the methods, witness lemmas) and never modifies
your file. Exit code 1 when something is underspecified, so it can sit in CI, or in an agent's
loop: --json gives the witness in machine-readable form, which is exactly the feedback an agent
needs to strengthen its contract.

Without access to the benchmark's oracle, it reproduces all 24 verdicts. Run on the whole
add_big file rather than just the main method, it also flags the three helpers Haiku wrote
(AddAbsolute accepts "10" + "10" = "201"): the weakness was not one slip, but the way the
whole file was specified.

Limitations, honestly

Small sample. 8 tasks per suite, one trial per cell, one agent family. The pattern is vivid, but it is a signal, not a measurement.
Complete is not correct. A contract can pin down a single, wrong result. The check removes specifications that are too weak, not ones that are mistaken.
The second-program trap. A postcondition like out == Model(ops), where Model reimplements the problem, is always "complete", and can carry the same bug as the code.
Witness search is heuristic. Neighbours come from simple rules; a contract can be incomplete in a subtler way and come out "inconclusive". Supported types for witnesses: int, nat, bool, char, string, seq<T>, tuples. Instance methods and heap-touching methods are skipped for now.

Prior work

After publishing, I did the literature pass I should have done before. The core idea is not new:
Shuvendu Lahiri's Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
(FMCAD 2024) already tests Dafny specifications symbolically, scoring their completeness by
mutating expected outputs on test cases and checking that the verifier rejects them. Related lines
of work include nl2postcond (completeness of LLM-written
postconditions measured against code mutants), Clover
(consistency between code, docstrings and Dafny annotations), and Lahiri's 2026
intent-formalization agenda, which names validating
specifications as the central bottleneck for AI-written code. Weak or vacuous specifications are
also a documented failure mode in recent verified-code benchmarks.

What dafny-complete adds is modest: it needs no tests or reference code (it runs the method
itself), it first tries a universal uniqueness proof, and it only reports a witness when Dafny
proves the contract accepts it. Details in the repo's
related-work note.

Why I care: Quod

This started as Phase 0 of Quod, a language designed to be
written by AI agents and checked by machines. The bet: everything that is expensive for humans
(exhaustive contracts, invariants, declared effects) is nearly free for an agent, so a language
can demand it.

This experiment changed the design. In Quod, the completeness check is built into the compiler:
an underspecified function does not compile, and the error comes with the witness. When
several answers are legitimately acceptable, you say so explicitly, with a relation between two
acceptable results:

fn binary_search(xs: &[i64], target: i64) -> Option<usize>
  requires sorted(xs)
  ensures ...
  loose (r1, r2) => r1.is_some() == r2.is_some()   // which index may vary; found/not found may not

Freedom becomes a visible, checked decision instead of an oversight.

Everything is open: the benchmark with every agent transcript, the language draft, and the tool
(Apache 2.0). If you write Dafny, I'd love to know what dafny-complete finds, or misses, on
your code. Issues and discussions are open at
github.com/quod-lang/quod.

What I learned using a 7B local LLM as the front end of a programming language

Malek AIT OUARET — Sun, 18 Oct 2026 12:50:01 +0000

Pseudocode is how we teach algorithms, yet it has never been executable. You can write "repeat divisor from 2 to 50"
on a whiteboard, but not run it. I wanted to change that without inventing yet another syntax, so I built
Pseudo.NET: you write pseudocode however you like, and a local language model turns it into a program.

This is not a launch post. It is what I learned about putting a small LLM at the front of a compiler. If you are
tempted to try something similar, maybe some of this saves you a few evenings.

The idea in one picture

free-form pseudocode  ->  local LLM  ->  JSON AST  ->  validate / repair  ->  deterministic C# backend  ->  normal build

The model never writes the final program. Its job ends at a structured tree (a JSON AST with a fixed set of node
kinds). Everything after that is ordinary, testable code: a validator, a type inference pass, and a backend that emits C#.
That split is the single most important design decision, and everything below follows from it.

Here is a program, written with tabs only, no braces, no end if:

We want to find all the prime numbers up to 50.

primes = a new list

define whether counter is prime, which returns a boolean
    isPrime = true
    if counter is less than 2 then
        isPrime = false
    repeat divisor from 2 to 50
        if divisor is less than counter then
            remainder = counter modulo divisor
            if remainder is equal to 0 then
                isPrime = false
    return isPrime

repeat counter from 2 to 50
    candidate = whether counter is prime
    if candidate then
        add counter to primes

print the text "Prime numbers up to 50:"
for each number in primes
    print number

The same program works written in French ("définir est-ce que compteur est premier…"), and in other languages the model
understands. The tool does not decide what the syntax is; the user does.

What I used

A small model, qwen2.5-coder:7b, run locally through Ollama. No account, no API key, and nothing leaves the machine (which matters if the users are students).
Temperature 0. For identical input, the output is the same.
F# for the compiler, C# as the target, and an MSBuild package so a .pseudo file builds like any other source file.

Lesson 1: a small model drops bare booleans

My first AST had flags like "tapped": true for keyboard input ("is the left arrow held or was it just pressed?").
The 7B model quietly omitted them. Not always, but often enough that games behaved randomly: a piece that should move
continuously moved once.

What worked was replacing flags by named values: "press": "held" or "press": "just_pressed", and for drawing
"style": "filled" or "style": "outline". A string with a name is much harder to forget than a missing true. Field
order mattered too: putting style right after kind made the model fill it in far more reliably.

A simplified example of what the model now returns for "while the left key is held":

{ "kind": "KeyPressed", "key": "left", "press": "held" }

Lesson 2: concrete examples beat abstract rules, but long prompts backfire

Rules written in prose ("a negated condition is a unary NOT") were followed inconsistently. A couple of tiny concrete
JSON examples in the prompt fixed the same problems more reliably.

The catch: every addition makes the prompt longer, and a longer prompt made the model forget something else. I added a
section about drawing and, a day later, noticed negations had regressed ("if not X" quietly became "X != false" and a game
showed a black screen). The only defence I found was a regression net: a script that regenerates a set of sample programs
from scratch with the real model and checks the generated C# against expectations. Every prompt change goes through it.
If you do this, build that net first, not after the third surprise.

Lesson 3: decide what you are allowed to repair

Models make mistakes in the shape of their output (a field named operator instead of op, a kind called Call
instead of FunctionCallStmt, an array where an object was expected). Repairing those is fine, and I do it in a small
normalisation pass.

What I refuse to do is repair the user's words: no keyword tables for "if / si / wenn" and no rewriting of text to
make the model's life easier. The moment I did that, I would have reintroduced a syntax, just a hidden one. So the rule is:

First choice: teach the model better, through the prompt.
Second: repair the shape of its JSON output.
Never: touch the wording of what the user wrote.

For what remains, there is a validator that checks the tree structurally. If it finds problems, the compiler sends them
back to the model for correction, at most twice. If the answer is still invalid, you get a warning, and the invalid answer
is never cached.

Lesson 4: determinism comes from caching, not from the model

Even at temperature 0, I do not want to depend on "the model happens to answer the same way tomorrow". Answers are cached
under a hash of (model + prompt + pseudocode), so an unchanged program never calls the model again, rebuilds are instant,
and the same input always gives the same C#. The six sample programs even ship their cached answer, so a first build works
without Ollama installed.

If you edit the generated C# by hand, the tool keeps your edit until the pseudocode changes, then regenerates and saves the
old file as a backup. The model is an interactive front end; the build stays boring.

What does not work (yet)

A 7B model is good, not perfect. Very long or ambiguous programs sometimes need rewording.
A model can be charitable: if a student writes something slightly wrong, it may guess the intent instead of flagging the mistake. For teaching this is a real question. I am thinking about showing the interpreted structure back to the student so they can check it.
Windows only for now, and the first generation of a new program takes seconds to minutes depending on your hardware.
It is a teaching tool. I would not use it for production code, and I would not trust the model for anything with security implications.

Is it a good idea?

For education, I think it is worth trying: the barrier to running an idea drops, and the generated C# is a real program a
student can open afterwards. For anything else, probably not, because a grammar is exactly the thing that makes a language
precise and predictable. I am deliberately trading that away, and the validator, the cache and the deterministic backend
are how I try to get some of it back.

Try it

Visual Studio extension: https://marketplace.visualstudio.com/items?itemName=pseudonet-lang.pseudonet
Without Visual Studio: dotnet new install PseudoNet.Templates
Source (F#, MIT): https://github.com/pseudonet-lang/pseudonet
Site: https://pseudonet-lang.github.io/

I would love to hear where it breaks, and whether you have tried a model as a parser rather than a chatbot.

Disclosure: I used an AI assistant to help draft and edit this article and to build parts of the tool. The experiments and conclusions come from my own work on the project.