DEV Community: Malek AIT OUARET

A compiler that refuses a contract that says too little

Malek AIT OUARET — Wed, 11 Nov 2026 12:30:36 +0000

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

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.