The intent gap is the alignment gap

date

May 4, 2026

slug

intent-gap

status

Published

A strange failure mode in verified code

Earlier this year, Nik Swamy's group at Microsoft Research used AI agents (Claude Opus 4.5) to produce 100,000+ lines of formally verified code in F*/Pulse — implementations of 52 algorithms from the CLRS textbook, each with separation logic proofs checked by Z3. Reader-writer locks. Dijkstra's algorithm. Prim's minimum spanning tree. All verified. All with machine-checked proofs.

Then they tested whether the verified code actually did what it was supposed to.

The answer, in 15% of cases, was no.

Swamy and Lahiri introduced SPOTs — Small Proof-Oriented Tests — simple concrete test cases like "does insert(table, key, value) actually insert the key?" They found that:

A verified hash table insert had a specification that allowed always returning false — the proof was correct, but the spec didn't require insertion to succeed

A verified Prim's algorithm had postconditions about array shapes but nothing about minimum spanning tree properties — you could return any spanning tree and satisfy the spec

A verified Dijkstra's algorithm initially only proved that distance(source, source) <= 0 — a trivially true statement that constrains nothing

These aren't bugs in the code. They're bugs in the specification. The code does exactly what the spec says. The spec just doesn't say what the programmer meant.

This is specification gaming

Anyone working in AI alignment should recognize this failure mode immediately. It is specification gaming — Goodhart's Law applied to formal verification:

When a measure becomes a target, it ceases to be a good measure.

The AI agent was optimizing for "produce code that the F* type checker accepts." It succeeded. The type checker accepted everything. But the specifications it generated were vacuous — formally correct, semantically empty.

This is structurally identical to:

An RL agent that achieves high reward by exploiting a loophole in the reward function rather than solving the intended task

An RLHF model that produces outputs the reward model rates highly without actually being helpful

A safety evaluation that passes because the model learned the specific test distribution, not because it's safe

The formal verification setting makes this problem visible in a way that the alignment setting doesn't. In alignment, we can't open up the objective function and inspect whether it captures intent — the objective is implicit, learned, or underspecified. In verification, the specification is explicit code. We can write a small test case and check: does this spec actually require the behavior we want?

The intent gap

Shuvendu Lahiri at Microsoft Research frames this as the intent gap: the distance between what a programmer (or an AI agent) means and what the formal specification says.

His group's findings quantify this gap across several approaches:

LLM-generated postconditions on real Java programs (Defects4J benchmark) caught 1 in 8 real bugs — but the other 7/8 had postconditions too weak to detect the fault

Auto-Verus used mutation analysis to score specification quality: mutate the code, check if the spec rejects the mutant. Without quality filtering, LLM-generated specs achieved only baseline proof accuracy. With filtering, accuracy improved 3.6x

TiCoder resolved intent ambiguity by generating test cases where different candidate implementations disagree, then asking the human to judge. This doubled correct code evaluation rates in a controlled study

The pattern is consistent: the bottleneck is not proof power, it's specification quality. Given a good spec, AI agents can produce verified code at scale. Given a bad spec, they produce verified nonsense.

Lahiri states it plainly: "The intent gap is the bottleneck; closing it will determine whether AI makes software more reliable or merely more abundant."

Replace "software" with "AI systems" and this is an alignment thesis statement.

Why this matters for alignment research

I see three concrete connections between specification quality in formal verification and the alignment problem:

1. Specification quality metrics are alignment metrics

The correctness gap I measure in LLMCodeProbe quantifies how often code satisfies a test suite without being correct. The specification gap that SPOTs reveal quantifies how often code satisfies a formal spec without being correct. Both are measuring the distance between "formally passes" and "actually does what we mean."

In alignment, we lack crisp versions of these metrics. We can't measure the distance between "the reward model scores this highly" and "this is actually helpful" because we don't have ground truth for "actually helpful." But in the code domain, we do have ground truth — we can run the code on concrete inputs and check. This makes program verification a productive testbed for developing and validating alignment metrics.

2. Specification gaming is reward hacking with a formal semantics

When an RL agent finds a reward hack, we usually can't explain precisely why the reward function was inadequate — we can only observe that the agent found an unintended behavior. When an AI agent produces verified code with a vacuous spec, we can point to the exact postcondition that's too weak and explain exactly how it fails to constrain the implementation.

This means we can study specification gaming in a setting where:

The objective (spec) is fully explicit and inspectable

The optimizer (AI agent + type checker) is deterministic

Failure modes are concrete and reproducible

We can formally characterize what "adequate specification" means (mutation-based spec quality, SPOTs)

These are properties we desperately want but don't have for RLHF reward models. Code verification gives us a simplified version of the problem where the science is tractable.

3. Intent formalization generalizes beyond code

The techniques that Lahiri's group develops for closing the intent gap — interactive disambiguation (TiCoder), specification quality metrics (Auto-Verus), behavioral testing of specs (SPOTs), translating natural language to formal specs (3DGen) — all generalize beyond code.

Interactive disambiguation is a form of active learning for specification elicitation. The same principle applies to RLHF: instead of labeling random preference pairs, find the pairs where candidate reward models disagree and ask the human to judge those.

Mutation-based spec quality checks whether a specification rejects incorrect implementations. In alignment terms: does the reward function actually penalize misaligned behavior, or does it only reward aligned behavior (which is a weaker guarantee)?

SPOTs validate specs against small concrete examples. In alignment terms: before trusting an evaluation benchmark, check whether the evaluation actually distinguishes good from bad on simple, interpretable cases.

A lightweight formal methods research agenda for AI safety

My own work sits at the lightweight end of this spectrum. Where RiSE MSR deploys F*, Z3, and separation logic, I use CrossHair (symbolic execution), Hypothesis (property-based testing), and boundary analysis — techniques that run on a laptop in seconds rather than requiring theorem prover infrastructure.

This tradeoff is intentional. For AI safety applications, we need formal methods that scale to evaluating thousands of model outputs, not methods that produce beautiful proofs of individual programs. The research agenda I'm pursuing:

Correctness gap measurement at scale. Run LLMCodeProbe on actual outputs from frontier models (Claude, GPT-4o, DeepSeek-Coder) across HumanEval + MBPP. Produce the first cross-model comparison of deep@1 alongside pass@1. Hypothesis: model rankings will change when we measure actual correctness rather than test-passing.

Specification gap metrics. LLMCodeProbe's benchmark dataset already includes postconditions and preconditions as structured fields, but they're not yet executable. Making them executable and measuring how often LLM-generated specs are trivially satisfiable would complement the correctness gap with a specification gap — how often does the LLM produce code that satisfies a meaningless spec?

Lightweight SPOTs. Generate small concrete test cases from postconditions and use them to validate specification quality before scoring solutions. This prevents the "vacuous spec" failure mode from inflating verification scores — the specification-level analog of test suite augmentation.

Self-repair via counterexamples. Feed LLMCodeProbe's counterexamples back to the generating model and measure whether it can fix the bug. This connects to the iterative refinement and debate paradigms in scalable oversight.

Formal verification researchers and alignment researchers are independently converging on the same insight: the hard problem is not building powerful optimizers — it's specifying what we want.

In verification, this manifests as vacuous specifications that pass the type checker. In alignment, it manifests as reward functions that don't capture human intent. The formal verification setting has a crucial advantage: we can inspect, test, and formally characterize specification quality in ways we can't for learned reward functions.

This makes program verification an underused testbed for alignment research. The problems are isomorphic, the tools are mature, and the feedback loops are fast. If we can't solve specification gaming in code — where we have formal semantics, concrete test cases, and ground truth — we're unlikely to solve it in the much harder alignment setting where none of these are available.

If you're working on formal methods for AI safety — specification quality, formal verification for ML systems, or lightweight safety guarantees — I'd like to hear from you. My work is at github.com/darshana-v.