Verified Specification as Code

A change request arrives, and it is one sentence: "let users share notes." In a healthy team this triggers a small ceremony. Someone updates the requirements document. Someone else remembers that the data model assumed one user per note and opens a ticket. An architect notes that every read now needs an actor and a permission the single-user design never carried, and that revoking a share needs its own path. A security reviewer asks, three weeks later, whether one user's share can expose another's data. Each is right to raise it. Collectively they are doing a job no one owns: holding a dozen documents consistent by hand, re-deriving by memory and meeting what a single sentence implied.

This is the same problem infrastructure had, before we fixed it. This essay traces one such sentence through a formal model, using user-to-user note sharing as the worked example, a per-resource permission question small enough to show the mechanism and a stand-in for the larger one, tenant isolation. The method scales because you formalise the small surface of load-bearing invariants, never the whole state, so proof-maintenance cost tracks the count of decisions, not product size: the honest answer to state explosion [the combinatorial blow-up that defeats exhaustive checking].

The claim, named before I argue for it: a formal specification does not merely flag inconsistency. It mechanically surfaces every proof obligation the change breaks, a precise, kernel-checked seed a human then classifies, each broken obligation either genuinely false and needing a respec, or still true and needing only re-proof. The blast radius [the set of obligations a change forces you to re-discharge] is the expert's expansion of that kernel-computed seed, not a list reconstructed from memory. What the model does not encode it cannot surface, so coverage completeness is a discipline you owe upfront, not a property the kernel grants.

Where the specification is now, infrastructure was fifteen years ago

Remember how bad infrastructure used to be; the forgetting is the proof that it worked. You provisioned a server by clicking through a console, or following a runbook by hand. The desired state lived in someone's head, in a stale wiki, and in the running machines, and the three never agreed. The gap had a name: drift [the silent divergence between what you intended and what is actually running], and the repair was a person reconciling intention to reality by hand, forever.

Infrastructure as Code [IaC] dissolved that, and how it did matters: the mechanism transfers. It made the desired state a file: declarative [you state what should be true, not the steps to get there], version-controlled, machine-reconciled. The system reads the file and makes reality match it; drift becomes visible because file and world can be diffed; a change becomes a pull request, not a memory. The human stops being the reconciliation loop and becomes the author of intent, the only part that ever needed a human.

The specification of a product is exactly where infrastructure was before that shift. Requirements live in prose, scattered across a requirements document, a backlog, a design file, a data model, and the heads of the people who were in the room. No canonical artefact a machine can check, so the reconciliation loop is staffed by humans, in meetings, indefinitely. A specification defect is disproportionately expensive because it propagates into prompt, code, and schema at once, with no compile-time comparator to catch it before it has replicated through everything built on top.

Name the move that closes this gap the way IaC closed the other. Verified Specification as Code: the specification of the product is a formal, machine-checked artefact; when it changes, the kernel re-checks every stated invariant against the current definitions and seeds the requirements, access rules, and second-order effects a human then expands; and code is built against it, the kernel type-checking the model while human review covers the code's conformance. The spec stops being a document you maintain and becomes a thing that maintains you, telling you the instant a change lands exactly what no longer holds. One boundary: IaC's reconciler rewrites reality to match the file; VSaC detects divergence between spec and proofs but does not rewrite the code. Detection transfers; remediation stays the developer's job and the coding agent's opportunity.

A word on the name. "Specification as Code" risks the loose DevOps reading, "everything as code" meaning "we keep our YAML in git." I mean something stricter. The load-bearing word is verified: a file checked by no one is just drift with better formatting. What makes this a category rather than a filing convention is that a kernel [the small, independently auditable core that mechanically certifies every logical step], not a reviewer, type-checks every stated invariant against the model's current definitions. The kernel is the sole trust root. The schema validator and the deterministic gates around it are convenience and enforcement, not trust: a buggy gate cannot forge a kernel pass it never obtained, it can only fail to block. For the properties the kernel does not cover, traceability and non-vacuity, which a True or sorry spec would slip past, a fail-open gate genuinely does let a bad commit through, which is why those checks are themselves committed, auditable, and adversarially reviewed.

The asymmetry that makes this urgent now

Coding agents have collapsed the cost of emission, producing a diff, from hours to seconds, while barely moving the cost of verification, convincing yourself the diff is correct. The agent that emits at full speed has neither the patience nor the stake to smooth an ambiguous spec over; it builds the ambiguity in every direction at once, with great confidence. So the binding constraint on shipping a correct product is no longer typing the code but knowing what correct means before the agent types thousands of lines against a spec that contradicts itself in three places nobody noticed. The highest-leverage move [the change that buys the most coherence for the least verification effort] is to make the specification small, formal, and checkable, so you verify the spec once rather than chase its contradictions through the code forever.

What it looks like in practice, and how long I have run each part

I am not describing an aspiration but a pipeline I have tightened for seven or eight months, in three layers that arrived in order, each closing a gap the previous one exposed.

Layer one: requirements as structured data, not prose. About five months. The first move is the least glamorous and the highest leverage: write requirements as records against a schema, not paragraphs. Every requirement gets an identifier, an owner, explicit acceptance criteria, a status, and its dependencies. The artefact is a prd.json [product requirements document] file, and a small tool standardises it so nothing is vague, duplicated, or quietly missing. A fragment, fully invented:

{
  "id": "REQ-014",
  "title": "A user can share a note with another user",
  "owner": "alice-chen",
  "status": "proposed",
  "acceptance": [
    "Given a note I own, I can grant another user read access",
    "The recipient sees the note in their list within one sync",
    "I revoke access and the note leaves their list within one sync"
  ],
  "depends_on": ["REQ-002"]
}

A schema is intolerant of what prose hides: a requirement with no owner, an acceptance criterion that is really three, a dependency on something deleted. Unlike BDD [behaviour-driven development] frameworks that couple acceptance criteria to a test runner and a fixed sentence syntax, the structured-record method is substrate-independent and composes cleanly with the Lean layer, one predicate per acceptance criterion, the link kept by naming discipline today and by generation once that gate lands. But a schema checks only the shape of each requirement, not whether two well-formed requirements contradict each other. For that you need a model.

Layer two: model the specification in Lean. The last couple of months. Lean 4 is a formal proof system whose kernel admits exactly one meaning per statement: any generator, tactic, agent, or person produces a candidate proof the kernel certifies or rejects. Express requirements as Lean definitions and propositions rather than English and two things become available no meeting can deliver: contradiction and ambiguity surface mechanically the moment they enter, not in a grooming session three weeks later; and "done" acquires a single, kernel-checked definition per requirement, rather than as many as there are people who read the sentence.

Return to the one-sentence change request, because here the parallel to IaC stops being analogy and becomes the actual machinery. The stand-in types below are minimal but genuine, and every fragment here was run through lake build, so compilability is verified rather than asserted:

-- Stand-in types; minimal but compilable
structure User where
  id : Nat
deriving DecidableEq, BEq

-- single-player: a note has exactly one user
structure Note where
  owner : User

Suppose the app began single-player, and somewhere early a requirement asserted that a note has exactly one user, which the code relied on for its audit log: every read was, by construction, a read by the owner. In Lean those invariants are definitions and theorems:

-- written when the app had one user per note
def canRead (n : Note) (u : User) : Prop := n.owner = u

-- single-player: revoking anyone is a no-op, since only the owner reads
def revoke (n : Note) (v : User) : Note := n

-- two theorems the audit and revoke flows relied on, proved once and forgotten.
-- both bodies are deliberately the simplest possible, so a later type
-- mismatch is visible rather than buried in tactic machinery.
theorem audit_actor_is_owner
    (n : Note) (u : User) (h : canRead n u) : n.owner = u := h

theorem revoke_preserves_read
    (n : Note) (v u : User) (h : canRead n u) : canRead (revoke n v) u := h

Now REQ-014 introduces sharing, and the first effect is a data-model commitment the kernel will not let you defer: Note has no field for a shared-user list, so you must decide what type carries that list and where it lives. Prose specifications defer this; formalising the capability forces it. REQ-014 edits the model in place, adding the field and rewriting the two definitions that read it:

-- REQ-014 edits the same file: Note gains a field...
structure Note where
  owner      : User
  sharedWith : List User

-- ...and canRead and revoke are rewritten to use it
def canRead (n : Note) (u : User) : Prop :=
  n.owner = u ∨ u ∈ n.sharedWith   -- ∨ = logical or; ∈ = is a member of

def revoke (n : Note) (v : User) : Note :=
  { n with sharedWith := n.sharedWith.filter (· != v) }   -- != = Bool-valued not-equal

These listings are the same file at successive moments, not one program you could compile end to end; the second structure Note, canRead, and revoke replace the first.

The payoff lands the moment Lean rebuilds: both earlier proofs are now not merely unproven but false. The intuition needs no Lean. A recipient can read a note they do not own, so audit_actor_is_owner is wrong; and revoking that recipient now changes what they can read, so revoke_preserves_read is wrong too. Two load-bearing assumptions, surfaced mechanically, neither remembered.

For the reader who wants the mechanism: on rebuild, each proof body := h reports a type mismatch, because h now has type n.owner = u ∨ u ∈ n.sharedWith, not the goal it used to discharge, so the proof term [the complete derivation a kernel certifies by type-checking] no longer type-checks. An unproved theorem might be waiting for more work; a false one cannot be rescued by cleverness.

The build flagged two broken theorems, one per load-bearing invariant that referenced the changed predicate, and here both are genuinely false rather than merely needing re-proof. That is the dial: every invariant you wrote as a theorem against canRead becomes a mechanically-detected consequence the moment canRead changes. The obligations the model misses are exactly the ones nobody formalised, invisible because an un-encoded invariant produces no failed proof, which is why layer three's gate refuses a predicate with no acceptance criterion and a criterion with no predicate. From those two broken obligations a domain expert expands the rest: the audit log has a second case; every access check now needs an actor and a permission, not an ownership test, so the app has acquired an ACL [access control list: a per-resource enumeration of explicitly permitted users] layer whether anyone wrote that requirement or not; and sharing opens a second-order question, whether one user's share can expose another's data, now a proposition someone must discharge rather than a risk someone must remember. The kernel did not enumerate those; it handed you the seed to expand from. That is the honest value, and it is still large.

This single-player to multiplayer fan-out [the cascading set of secondary effects triggered by a single change] is tribal knowledge in a prose specification; in a formal specification it surfaces as broken proof obligations, without a meeting. That is the heart of the claim: not that Lean is rigorous, although it is, but that change propagates as broken proof obligations that seed the work, not a document to re-read from memory.

The honesty inflection. What went wrong in the middle is the most common failure of this method, and the easiest to fake. Early formal specs of mine were vacuous [structurally present but empty of real content]: acceptance criteria encoded as the proposition True, structural theorems left as sorry [Lean's placeholder for an unproved claim, which compiles but proves nothing]. They compiled. The build passed. They verified nothing, because a proof of True holds equally for every proposition. An adversarial check, refute-first [seeking counterexamples before trusting their absence] rather than confirm-first, caught it, and the repair was to rebuild the modelling so predicates carry real, decidable content, predicates like canRead which, with a DecidableEq User instance in scope, the kernel can reduce to a definite true-or-false by computation, and the build fails honestly when a requirement is unmet. Formal-verification theatre is worse than no verification, because it launders the same uncertainty under a green tick.

Layer three: enforce it so the discipline cannot drift. About three weeks. A discipline that depends on a human remembering to run it is already drifting, so the final layer makes the rules non-committable through deterministic gates wired into the commit path. A gate is a pre-commit or CI check that blocks a commit outright rather than warning: one rejects a commit referencing a requirement identifier absent from the structured spec; another fails the build when a Lean predicate's name has no matching acceptance-criterion identifier in prd.json. Both match identifiers, which is mechanical; whether a predicate captures its criterion's meaning is the by-inspection step, not yet generated. The first gate runs today; the second is younger and in places still illustrative. An override by a named authority is a committed, documented reason, not a quiet bypass. The loop is only closed when "the spec was checked" is itself enforced, not trusted, exactly as IaC is worthless if anyone can SSH in and change the server by hand.

The strongest objection, and the harder ones behind it

The first objection comes from the people closest to the agents: you do not need a kernel, you need tests. Run a comprehensive eval suite in a loop, or let an LLM judge whether the spec is coherent, and you get the same assurance without learning Lean. It fails on first principles. Tests and evals sample behaviour: they show the presence of a property on the cases you thought to write, and an agent emitting at full speed passes every test it can see while violating an invariant no test names. They cannot decide the absence of contradiction across the whole specification, which is exactly what a change request probes. The serious version of this objection is not evals but bounded model checking and SMT [satisfiability-modulo-theories solvers], TLA+ and Alloy, which do decide absence of contradiction, but only over a bounded state space and best on concurrency and temporal properties. The kernel buys something different: it certifies unbounded propositions and composes proofs across an evolving spec, so the falsified-proof-on-edit propagation, not exhaustive state search, is what you pay for. An LLM judge is the weak version: it reintroduces the uncertainty you are paying to remove, can be wrong with complete confidence, and returns a verdict neither reproducible nor adversarially auditable. A kernel's verdict is both. Where evals genuinely win, the behavioural surface and runtime drift no static spec captures, keep them as the complement, not the coherence authority.

A second objection cuts at adoption: your customer will not read Lean, and most teams cannot write it, so you have moved the bottleneck rather than removed it. Correct about the surface, wrong about the structure. Two motions hide inside "customer" here: a team that builds software runs the formal layer itself, while an organisation that buys the software never writes Lean and consumes the signed human-readable view and the consequence report as governance evidence. Both are served by a two-layer design: a machine layer the kernel checks, and a derived human-readable view any stakeholder reads, the prose requirements and the plain-English definition of done. Today a naming and derivation discipline keeps them aligned, with drift caught by inspection; full generation, so the two provably cannot disagree, is the next gate. The customer signs the view, and that inspectable view is the audit artefact their risk and governance functions need, now derived mechanically rather than assembled by hand. Regulated buyers do not drop process around a new source of truth, they add it; the coherence evidence is just cheaper to produce.

A harder objection sits behind it, technical. The kernel type-checks every stated invariant against the model's current definitions; it does not establish global consistency, since a latent contradiction stays unflagged until someone tries to derive it. Nor does it verify the correspondence between model and intent. A predicate that is internally consistent but encodes the wrong thing carries a green tick and is more dangerous than the equivalent wrong sentence in prose, because it looks verified. The defence is refute-first discipline at the encoding step: for each predicate, can you construct a scenario that should satisfy the criterion but fails the predicate, or vice versa? If yes, the encoding is wrong and a green build is a false signal. The structured-requirements layer makes this tractable: each Lean predicate traces back to one named acceptance criterion in plain English. The correctness question becomes local and reviewable, one predicate against one criterion, a question you can put to any engineer who reads prose without knowing Lean. What it does not yield is a mechanical witness: whether a predicate faithfully encodes an English sentence is finally an interpretive judgement. The structure makes that judgement small and located; it does not remove it. Because the kernel cannot police encoding fidelity, the named owner of each acceptance criterion co-signs its predicate mapping in the pull request, so a human is accountable for the one judgement the machine cannot make.

Another objection is ownership: if one person must write and maintain Lean, it may recreate the same single-point dependency in a new language. The answer is scope discipline and a steward model. You formalise the load-bearing slice, the permission model and the key invariants, small enough to own clearly. A tech lead or principal holds commit authority on the formal layer; others propose changes via pull request. The bus factor [the number of team members whose departure would jeopardise progress] is one for authorship, not for comprehension: the prose view and the JSON requirements layer are readable without Lean, so the team audits intent even if it cannot write proofs. If the steward departs, the slice is bounded by design, so a successor relearns a small, named surface, not a sprawling second codebase. Writing non-vacuous Lean is a real skill learned over months, so this is no same-week swap; the win is bounded scope.

The last objection is historical and therefore the most stubborn: formal methods have been the advocated answer since Dijkstra and Hoare. TLA+, Coq, Z, Isabelle and their descendants were each the technology that would finally make software verifiably correct. None achieved general adoption in product engineering. Why now? Because adoption is an asymmetry problem, not purely a tooling problem. Tooling did improve materially: Lean 4 brought ergonomics, a language server, and in Mathlib [Lean's single unified mathematical library] a single actively-maintained corpus where earlier ecosystems, Isabelle's archive and the Coq libraries, offered loosely-coupled collections, and LLM-assisted tactics lowered the cost of proving routine obligations. But those improvements narrow the gap, they do not cross it. What crosses it is the asymmetry this essay opened with: the slow human author who absorbed an imprecise spec over time is gone. The formal tooling became adequate at roughly the moment emission became cheap; the two shifts arrived in the same decade. The reflexive counter, that cheap emission should reduce the urge to formalise, why prove it when you can re-emit and test in seconds, gets the dynamics backwards: empirical iteration converges only on the properties your tests name, so an agent emitting confident contradictions where no test looks makes regenerate-and-test diverge, not converge. Cheap emission raises the value of a fixed point, the spec, rather than lowering it.

For a team running any Agile cadence today

The same argument holds at a less formal layer, where a head of technology owns the mandate that spec changes require a consequence report before code begins. The formal layer is not a replacement requirements tracker: your existing ALM [application lifecycle management] or issue tracker keeps workflow, assignment, and status, while the structured spec holds only what 'done' and 'consistent' mean, the two linked by the requirement identifier. Two properties fall out. The override-by-named-authority bypass is already a segregation-of-duties and audit-trail primitive, since every exception is a committed, attributable, time-boxed record, and a rising override rate is itself a monitored signal of a mis-scoped gate rather than a steady state; and the consequence report, kernel-seeded and today expanded by hand with mechanical generation named as the next gate, is the change-control evidence a change advisory board or auditor asks for before a release. Deliberate change to the model is itself a governance act, because the model is the source of that report.

None of this asks you to abandon the goals of your ceremonies, only to change the mechanism. Story refinement exists partly to detect and resolve contradictions between requirements; a formal spec does that on every change, in seconds, by failing to build when two collide, so the meeting shortens rather than disappears: the domain-knowledge work, surfacing what stakeholders actually want, stays human; the coherence work, discovering what contradicts what, becomes mechanical. The result is not less rigour and fewer meetings as a trade. It is more rigour and fewer meetings, because you moved the rigour out of human attention, which is scarce and forgets, and into a kernel, which is cheap and does not.

The practical first step, and it needs no Lean. Adopt structured requirements before anything formal: identifier, named owner, explicit acceptance criteria, schema-validated. This pays in week one, surfacing coherence problems as schema errors. Formalise the load-bearing slice next, enforce last; each layer earns the next.

What exists today, plainly

In the spirit of not laundering aspiration as fact: the structured-requirements layer is shipped and has run for months across real work. The Lean modelling layer is shipped, recently rebuilt to kill vacuity, and proves real obligations on real specifications, though the report mapping a failed proof to a plain-English obligation list is still generated by hand. The enforcement layer is young, a few weeks live, and earning its keep. The single-player to multiplayer example here is a faithful illustration, written with invented code so it leaks nothing; the mechanism it illustrates is real and runs. I would rather you knew the edges than believed a rounder story.

The reconciliation loop, closed

Infrastructure as Code did not make servers interesting. It made them boring, the highest compliment you can pay infrastructure, by removing the human from the reconciliation loop and leaving them only the part that needed a human: stating intent. The product specification is the most consequential place that loop still runs on human memory, in meetings, indefinitely. We have the tools to close it. A specification can be a file. A file can be checked. A change can surface its own consequences, mechanically. And once it does, the team stops staffing the coherence half of that loop by hand and spends its attention on the only thing that ever needed people: deciding, on purpose, what the thing should be.

This essay is the thesis of the "Verified Specification as Code" series. "Requirements as Data" is layer one, why a schema beats prose for the record that carries intent. "When the Spec Can Contradict Itself" is layer two, the contradiction-finding machinery a schema cannot reach. "Continuous Enforcement and Continuous Verification" is the runtime counterpart, checking the records on every change rather than when someone remembers. "When the Document Leaves the Factory" is the two-reader design for stakeholder-facing output, and "Holding Water with Our Hands" applies the same reconciliation-loop argument to statutory compliance.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.