When the Spec Can Contradict Itself

A one-line change request lands in your tracker: "let a busy checker hand their sign-offs to someone else." A reviewer reads the diff, nods, and merges. The author is satisfied. The reviewer is satisfied. And eighteen months earlier, on a screen nobody has open, a rule was written that this change has just falsified: that the person who signs off a unit of work is never the person who wrote it. Nobody remembers the rule. The code is now wrong in a way no one can see, because the thing it contradicts lives in prose, in memory, in none of the places the merge button can check.

Picture a different arrangement. Every rule the product depends on is not a sentence in a document but an answer submitted to an examiner. This examiner has one trait that makes it useful and one that makes it dangerous, and most of this essay is about telling the two apart. The useful trait: it cannot be flattered, hurried, or bribed by a green tick. It reads every step of your reasoning and certifies the result only if the result genuinely follows. The dangerous trait: it grades the question you wrote down, not the question you meant. Get those two straight and you hold the whole of formal specification, its power and its single failure mode, in one image.

The examiner is a proof kernel [the small, independently auditable core of a proof system that mechanically certifies each logical step]. The generator that hands work to it can be an agent, a tactic, or a tired human at midnight, and can be as clever as it likes, because the kernel does not trust it; it re-checks the finished derivation itself. That asymmetry, a powerful untrusted generator and a small trusted checker, is why this scales: you can throw an arbitrarily strong prover at the examiner without ever trusting the prover. This essay is the layer-two deep dive of a series; the thesis that the product specification belongs under machine check, as infrastructure already does, is argued in the flagship. Here I show the examiner at work, in Lean 4, including the two places it earns its keep and the one place it will quietly betray you.

A requirement is a definition and a claim about it

Start with the rule the change request was about to break. In a task app, every task has an author and a checker who signs it off, and a separation-of-duties [the control that the maker of a thing cannot also be its checker] rule says the two are never the same person. In prose that is one sentence. In Lean it is a structure, a definition, and a theorem.

structure User where
  id : Nat
deriving DecidableEq, BEq

-- A unit of work: who wrote it, who signs it off.
structure Task where
  author  : User
  checker : User

-- Separation of duties: the checker is never the author.
def separationOfDuties (t : Task) : Prop := t.checker ≠ t.author

-- When only the named checker can sign off, "who may sign off"
-- is a single, decidable test.
def canSignOff (t : Task) (actor : User) : Prop := actor = t.checker

Now the rule the audit log silently relied on: a signer is never the author. That is a theorem, proved once and forgotten.

theorem signer_not_author
    (t : Task) (actor : User)
    (sod : separationOfDuties t) (h : canSignOff t actor) :
    actor ≠ t.author := by
  unfold canSignOff at h     -- h : actor = t.checker
  subst h                    -- replace actor with t.checker
  exact sod                  -- goal is now t.checker ≠ t.author

Three lines, and the kernel certifies them. Note what has happened that no meeting delivers. The word "done" now has exactly one meaning per requirement, the predicate, and the rule the audit log depended on is not a hope in a senior engineer's head but a checked proposition [a statement the kernel can certify true or refute]. The definition of canSignOff is the load-bearing one, and we are about to change it.

The contradiction surfaces as a failed build

The change request adds delegation. A checker may hand sign-off authority to another user, so "who may sign off" gains a second case.

-- REQ-027: a checker may delegate sign-off authority.
-- `delegatesTo a b` means a has handed their authority to b.
def canSignOff (t : Task) (actor : User)
    (delegatesTo : User → User → Prop) : Prop :=
  actor = t.checker ∨ delegatesTo t.checker actor   -- ∨ is logical or

The moment this definition lands, signer_not_author stops building. The shallow reason is arity: canSignOff now takes a third argument, so the old theorem no longer type-checks at all. The deep reason matters more, and it survives any cosmetic repair of the signature: the theorem is not merely unproved, it is false. You can hand the examiner a witness to its falsehood.

def aliceAuthor : User := ⟨1⟩
def bobChecker  : User := ⟨2⟩
def t : Task := { author := aliceAuthor, checker := bobChecker }

-- A delegation that routes sign-off straight back to the author.
def delegatesTo : User → User → Prop :=
  fun a b => a = bobChecker ∧ b = aliceAuthor

-- The author can now sign off her own task, while SoD still "holds".
example : canSignOff t t.author delegatesTo := by
  right
  exact ⟨rfl, rfl⟩

Hold the distinction between false and unproved, because for this audience it is the whole game. An unproved theorem might just be waiting for a cleverer tactic; you keep working. A false theorem cannot be rescued by any amount of cleverness, because a counterexample exists in the model. separationOfDuties t is still true, the named checker differs from the author, yet the author can sign off her own work through a one-hop delegation. The examiner will never certify signer_not_author again, and that refusal is the system telling you, in seconds and without a meeting, that two requirements now contradict each other.

The build flagged one red proof. What a domain expert reads off that single failure is a fan-out [the cascade of secondary effects a single change triggers]: delegation chains can be longer than one hop, so the real rule is about reachability [whether any chain of delegations connects two users], not a single edge; revocation now has a second path; the audit log must record the acting delegate, not the nominal checker; and delegation cycles are suddenly a proposition someone must rule out rather than a risk someone must remember. The model did not enumerate all four for you; it gave you the one contradiction from which a competent person expands the rest. In a prose specification that fan-out is tribal knowledge, recovered by whoever still works here. In a formal one it is a red build.

Three ways a passing build can still lie

Here I have to be straight with you, because this method's failure mode is more dangerous than prose's. A green build is not proof that you verified anything real. There are exactly three ways the examiner hands back a pass that means nothing, and a serious practitioner learns to smell all three.

The trivial question. You encode an acceptance criterion as the proposition True.

def sodOk : Prop := True
theorem sod_holds : sodOk := trivial   -- compiles, proves nothing

A proof of True transfers to no obligation whatever; it holds equally for a correct product and a broken one. The build is green because you asked the examiner nothing.

The blank answer stamped "trust me". You state the real proposition and leave its proof as sorry [Lean's placeholder for an unproved claim, which compiles but discharges nothing].

theorem sod_holds' : separationOfDuties t := sorry

This is worse than the first, because the proposition looks substantive. The kernel emits a warning, but the build still produces an artefact, and a warning nobody reads is a lie nobody caught.

The wrong question, faithfully answered. This is the deep one, and I return to it below. You write a predicate that is internally flawless and encodes the wrong rule. The examiner certifies it perfectly. The green tick is real and the meaning is wrong.

The shared antidote to the first two is a discipline, not a tool: refute-first [actively trying to construct a counterexample before trusting that none exists]. For every predicate, before you believe a passing build, you try to inhabit its negation. If separationOfDuties were vacuous, you would ask the examiner to prove ¬ separationOfDuties t for an arbitrary task and watch it succeed, which tells you the predicate constrains nothing. A green build is the start of the audit, not the end of it. I rebuilt an entire formal layer of my own once after a refute-first pass found it riddled with the first two patterns; the build had been green for weeks and had been proving, precisely, nothing.

The decidability boundary: what you can hand the examiner

Not every claim can go on the exam. The examiner can mechanically decide [evaluate to true or false by computation] some propositions and merely check a hand-written proof of others, and the line between them shapes how you model.

Equality of users is decidable, because User derives DecidableEq, so membership in a finite list of checkers is decidable too, and you can ask for a verdict by computation:

#eval decide (aliceAuthor = bobChecker)   -- false, mechanically

Now recall that the real delegation rule is about reachability, not a single hop. If you bound the chain length and model delegation as a finite edge list, reachability stays decidable, because it is a terminating computation over finite data:

-- Bounded reachability over a finite delegation graph: decidable.
def reaches (edges : List (User × User)) : Nat → User → User → Bool
  | 0,   a, b => a == b
  | n+1, a, b => a == b ||
                 edges.any (fun e => e.1 == a && reaches edges n e.2 b)

But the instant you state the rule the way a security reviewer actually means it, "there exists a delegation chain of any length routing sign-off back to the author", you have quantified over an unbounded set, and decide can no longer close the goal on its own. You are now on the proof-checking side of the line, not the deciding side. To get back, you finitise: make User a Fintype [a type with finitely many elements, which the kernel can exhaust], bound the search by the node count, and prove termination. The boundary is not a defect, it is information. A rule you cannot put on the exam without finitising is a rule whose unbounded version you were quietly assuming was safe, and the friction of formalising it is the model refusing to let you assume that for free. Continuous quantities, real-valued thresholds, and search over infinite spaces sit on the far side of this line; crisp, finite, combinatorial rules sit on the near side, and the kernel decides them outright. Knowing which rules fall where is most of the skill.

Two readers, one source

The obvious objection from the business side is that no stakeholder will ever read reaches, and they are right, so they never should. The output is two-layered: a machine layer the kernel checks, and a human-readable view generated from it. Each predicate is registered with a plain-English gloss and a named owner, and a generator walks the formal layer to emit the requirements document and its definition of done. Because the prose is a projection [a derived view computed from a single source] of the formal layer, the two cannot drift; you do not maintain them in parallel, you maintain one and compute the other.

-- The formal predicate carries its own human gloss and owner,
-- so the prose requirement is generated, not hand-written.
structure Spec where
  name  : String
  owner : String
  gloss : String          -- the sentence the stakeholder signs
  holds : Task → Prop

I will keep the honesty register the series demands: in my own pipeline this generation is the next gate, not yet automatic. Today a naming and traceability discipline keeps the prose aligned, and drift is caught by inspection rather than mechanically. The design invariant, one source projected two ways, is in place; its enforcement is not.

The objection that actually bites

The shallow objection is "most teams cannot write Lean," which layer one of this series answers: adopt structured requirements first, with owners and acceptance criteria, and that pays before any proof exists. The objection this audience will press is the third lie above, and it is not about scale. It is about soundness of encoding.

The examiner certifies the internal coherence of your model. It says nothing about whether your model means what you intended. Suppose the true rule is "no delegation chain may route sign-off back to the author," but you encode the simpler t.checker ≠ t.author, the static rule from before delegation existed. That predicate is internally flawless, and the kernel certifies it forever. It is also the wrong rule: it passes exactly the broken delegation that detonated this essay. A green tick on a wrong predicate is strictly more dangerous than a wrong sentence in prose, because it looks verified, and people stop reading verified things closely.

No tool closes this gap, because it is the gap between formalism and intent, and it cannot be formalised away. There is a discipline that bounds it, and it is the same refute-first move run at the encoding boundary rather than the proof boundary. For each predicate you ask: can I construct a scenario that should satisfy the rule the owner agreed to, but fails this predicate, or the reverse? For t.checker ≠ t.author the answer is yes in one line, the delegated case, which tells you the encoding is wrong before a single proof is written. The structured-requirements layer is what makes this tractable at scale: every predicate traces to a named criterion in plain English with a named owner, so the audit question collapses to "does this predicate faithfully encode the rule its owner signed?" That has a yes-or-no answer, and you can put it to any engineer who reads prose, without their knowing Lean. The kernel cannot ask it for you. Nothing can. But the kernel makes every other question mechanical, which is what frees a human to spend their scarce attention on the one question that is irreducibly theirs.

What exists today, plainly

In the spirit of not laundering aspiration as fact: the modelling shown here is real and runs, recently rebuilt to kill exactly the vacuity the three-lies section warns about. The decidability boundary is lived, not theoretical; I have hit the unbounded-reachability wall and paid the finitisation cost to climb back. The two-reader generation is designed and partly built, the prose view kept aligned by traceability discipline today rather than by a closed mechanical gate. The delegation example is invented end to end so that it leaks nothing, but the mechanism it shows, a contradiction surfacing as a red build the instant it enters, is the daily behaviour of the thing, not a hope about it.

The examiner's most useful verdict

Return to the examiner. We tend to prize the pass, and the pass is worth having only once you have learned how easily it lies. The verdict that earns the examiner its place is the fail, delivered the moment a change falsifies a rule written long ago by someone now forgotten, instead of a quarter later in an incident review. An examiner that cannot be flattered is not a bureaucrat in your pipeline. It is the one reader who has actually read every rule you ever wrote down, every time, and who tells you, before the agent has typed a thousand lines against a contradiction, that the spec you just changed no longer agrees with itself. The cost of that reader is that it grades only what you write, not what you mean. Pay it with refute-first discipline at the encoding boundary, and you have moved the one job that needs a human, deciding what the thing should be, out of the reconciliation loop and into the open, where it belongs.

This is the layer-two deep dive of the "Verified Specification as Code" series. It sits beneath the flagship "Verified Specification as Code" (the thesis: the product specification belongs under machine check, as infrastructure already is), alongside "Requirements as Data" (the no-Lean on-ramp), and ahead of "Continuous Enforcement and Continuous Verification" (the runtime half of the same loop). The sibling essay "When the Document Leaves the Factory" develops the two-reader design in full.

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.