How High Can You Build in Mud?

A mud hut is a good building. It is cheap, made of what is already on the site, warm in the cold and cool in the heat, and when it cracks the person living in it can repair it with their hands. Millions of people live well in earth construction and always have. Anyone who sneers at it has confused a material with a failure.

So this is not an argument against mud. It is an argument about height.

You cannot build a hundred storeys in mud, not because mud is shameful but because mud has no datasheet. Nobody can tell you, in advance and in numbers, what a given batch will bear. Steel can. An engineer opens a table, reads a yield strength and a modulus, and calculates whether the building stands before anyone digs. That table is what lets one person stack a hundred floors without re-deriving the behaviour of every beam.

One qualification, which turns out to be the most useful part of the analogy: that engineer does not build to the calculated limit. They apply a safety factor and build to a fraction of it, because the calculation is trusted and the world is not. Loads get misjudged, materials vary, someone eventually puts a swimming pool on the roof. Calculation plus margin beats judgment alone, and it does not abolish judgment. Anyone claiming otherwise is describing a discipline they have not practised.

The same limit governs specifications. A product requirement written in prose, a contract clause, a policy: these are mud, often excellent mud. But there is a height beyond which they will not go, and that height is not a matter of taste or diligence. It is a number.

The number

Take a specification of n requirements. What eventually hurts you is rarely a single bad requirement. It is two good ones that cannot both be true. Requirements do not fail alone. They fail in pairs.

The count of pairs is n(n−1)/2. Ten requirements give forty-five, which one competent person can hold across a careful afternoon, and this is why small specifications written by careful people genuinely do work. Fifty give 1,225. A hundred give 4,950.

Now the honest objection, and it matters: almost all of those pairs cannot possibly conflict. A requirement about audit logging and one about button placement do not interact, and no reviewer wastes a second on them. The quadratic count is an upper bound on the conflict surface, not its size. If the argument needed all 4,950 pairs to be live, it would be wrong.

It does not, and the real version is worse. You cannot tell which pairs interact without already having done the analysis. Two requirements conflict when they share a referent, and sharing is transitive through the model: R1 mentions users, R7 mentions accounts, R23 says every account has an owning user, and now R1 and R7 interact through a chain nobody was holding in mind. The pairs a reviewer naturally checks are the ones that obviously relate. The pairs that bite relate through two or three hops, which is precisely the set that looks unrelated on the page.

Nor is it only pairs. Three requirements can be consistent two at a time and jointly unsatisfiable, so pairs are the floor of the problem rather than its ceiling.

Set against that, human review is linear in n. You go down the list, considering each requirement against the handful of others you happen to be holding. Linear attention against a surface that is at least quadratic and whose live subset cannot be identified in advance. The curves cross, and afterwards the gap widens with every requirement you add: the proportion of your specification actually checked is falling while your effort rises.

That is the height limit of mud, in numbers. It sits roughly where one person can no longer hold the whole interaction surface at once, which is to say somewhere around one storey.

Why care does not save you

The obvious response is to try harder. Better reviewers, more of them, a template, a checklist.

It does not work, because contradictions do not announce themselves at the moment they are written.

Consider two requirements, each impeccable alone.

R1. A user may export their own data at any time. R2. Records subject to a legal hold must not leave the system.

Neither contains an error, and both survive any review that considers them one at a time, which is what almost every review is. The error is in the space between them, and that space is not on the page to be read.

You meet it when a user under legal hold clicks Export: at implementation, or worse, in production.

There is a well-worn claim that defect cost rises by an order of magnitude per phase, and it needs handling carefully, because the famous table with its neat 1, 6.5, 15, 100 is widely criticised as folklore nobody can trace to a study. The version that survives is weaker and sufficient: the direction is robust where the magnitude is not, and Boehm and Basili still put post-delivery fixes at roughly a hundred times a requirements-phase fix in 2001. In fast-cycle work the curve is flatter. It slopes the same way.

That is all the argument needs, and note what it implies. A contradiction invisible during specification review is not merely likely to surface in the expensive part of the curve. It is guaranteed to, because the cheap part had no instrument that could see it.

So the problem is not insufficient care. Care is a linear instrument, and no quantity of it changes the shape of the curve.

Sampling against quantifying

Here the argument meets a reasonable objection: we already have instruments. Tests. Code review. A well-designed requirements template.

All real, all worth using. But they share the property that decides the matter.

They sample the interaction surface. They do not quantify over it.

A test picks a point. A reviewer picks the pairs they happen to think of. A template constrains the shape of each requirement while saying nothing about the relations between them. Each inspects a subset, and its value depends entirely on whether that subset happened to include the pair that was going to hurt you.

A type checker, a schema or a proof kernel does something categorically different. It considers every case in the space it ranges over, including the ones nobody could have thought to consider, and it does not need to guess which pairs are live because it does not proceed pair by pair at all. Sampling against universal quantification is the same distinction as testing against proof, and it is the actual content of the mud-and-steel metaphor.

Two limits must go on the record, because without them the claim is false.

Decidability. Consistency checking is not decidable in general; give a checker an expressive enough logic and it can run forever without answering. What is decidable are restricted fragments, and the discipline is keeping your requirements inside one: finite domains, decidable predicates, quantification over enumerable sets. That excludes real requirements. "The system shall behave reasonably under load" is not going into a decidable fragment, and pretending otherwise is how this field earned its reputation.

A proof assistant does not detect contradiction by falling over. Most advocacy gets this backwards. Encode two conflicting requirements as axioms and Lean does not complain, it builds. Worse, from a contradiction everything follows, so every theorem you subsequently "prove" is worthless while the build stays green throughout. Inconsistency is silent, and a green build is not evidence of anything.

The discipline is therefore not "write it in Lean". It is: encode requirements as definitions and decidable predicates that get evaluated, never as axioms that get assumed. Then a conflict is not an inconsistency lurking in your assumptions, it is a proposition that evaluates to false, which is loud, immediate and local.

For R1 and R2:

-- Compiles as-is on Lean 4.29.1. No imports, no sorry, no axioms
-- beyond Lean's own. Paste it into a file and run `lean` over it.

abbrev UserId := Nat

structure Doc where
  owner  : UserId
  onHold : Bool
deriving DecidableEq

-- R1: a user may export a document they own
def mayExport (u : UserId) (d : Doc) : Bool := d.owner == u

-- R2: a document under legal hold must not leave the system
def mustNotLeave (d : Doc) : Bool := d.onHold

-- The two requirements, checked against each other over the domain
def specConsistent (ds : List Doc) : Bool :=
  ds.all (fun d => !(mayExport d.owner d && mustNotLeave d))

-- Evaluated, not assumed. A document both owned and held makes this
-- false, and it is false on the day R2 is written.
example : specConsistent [{ owner := 1, onHold := true }] = false := by decide

The important word is decide. The machine is not asked to trust a claim but to compute one, and the answer arrives in seconds, naming both parties to the conflict.

Be clear about what those twenty lines do not establish, because the gap is where this field loses people. They show the two requirements are jointly unsatisfiable for a document both owned and held. They do not show the requirements are the right ones, do not check any document outside the list you handed them, and say nothing whatever about the system you are going to build. The claim is only that this scales to n where reading does not, and that the marginal pair costs you nothing.

You did not become more careful. You changed instrument.

What actually just changed

Formal methods are not new, and honesty requires admitting why they stayed niche: they lost on price. The proof cost several times what the thing cost, so outside avionics, rail signalling and chip design the arithmetic never closed.

Generation got cheap, and that is the part which is genuinely new rather than eternally true. A language model will draft the formal statement, propose the model and attempt the proof. What it will not do is decide whether the result is correct, and that is exactly the part that did not need to change: the kernel checks the finished derivation and does not care who produced it. A powerful untrusted generator feeding a small trusted checker is a very old and very good architecture, and cheap generation is the input it was waiting for.

The expensive half collapsed while the soundness of the cheap half stayed put. The reason to reach for formal specification in 2026 is not that the argument improved. The bill got smaller.

What the bill still is. Cheaper is not free, and an essay that skips the cost side is advocacy rather than engineering.

Choosing the model is now the expensive step and it is not automatable: deciding that a document has an owner and a hold flag, rather than six other defensible schemas, is the decision everything else depends on. Keeping the specification aligned with the code is a standing obligation, and a spec that has drifted is worse than none, because it is confidently wrong and people trust it. And someone must be able to read the thing; if that is one person you have built a bus factor of one out of the artefact meant to reduce risk.

My honest split: modelling decisions take most of the human time, proof effort takes most of the machine time, and drift maintenance is the cost nobody budgets for and everybody pays. A much better bill than 2015 offered. Not a small one.

The objections that actually bite

Not "this is too hard" and not "nobody will read Lean". These three.

First: verification does not remove error, it relocates it.

Prove your specification consistent and you have proved something about your model of the world, not about the world. Bridges rarely fail because the steel was weaker than the datasheet said. They fail because of the ground, the water, the load nobody modelled, the assumption so universal that no one wrote it down. Formalisation moves error out of implementation and into specification, and specification is where the genuinely hard problems live.

This is true, and any essay pretending otherwise deserves to be ignored.

But look at what the relocation buys. Ambiguity in a prose clause is distributed: it lives in every reader's head, differently in each, undetectable until two of them act on incompatible readings, at which point the disagreement is about what a sentence meant and has no procedure for resolution. Ambiguity in a formal definition sits on one line, has a name, and can be argued about by people who agree on what they are arguing about. The claim is not that formal specification makes you right. It makes disagreement locatable, and given the alternative surfaces in production or in litigation, that is a large prize for an honest concession.

Second: a consistent specification is not a working system.

None of the above establishes that the code implements the specification, and that gap is most of the work. The reference point is seL4, the microkernel whose functional correctness was machine-checked from specification down to its C implementation in 2009 at NICTA in Australia. What makes it the landmark is that it closed the gap; what makes it sobering is the price, years of a specialist team for a kernel of some thousands of lines. Almost nobody pays that.

So be precise about what the cheap version buys. Checking that a hundred requirements are mutually satisfiable is worth doing and is now nearly free. It tells you the thing you asked for is a thing that can exist. It tells you nothing about whether you built it. Anyone saying "formally verified" without finishing the sentence, verified against what, is either confused or selling.

Third, the one I opened with: most software should be a mud hut, and most requirements documents should stay prose. The question was never mud or steel as a matter of principle. It is what you are putting on top, and who is standing underneath.

The criterion

First, drop the binary. Mud and steel are the ends of a range and almost everything worth building sits between. A schema that rejects a malformed requirement costs a morning. A type system that makes an illegal state unrepresentable costs a design conversation. Property-based tests generating a thousand cases at a boundary cost an afternoon and sample far better than examples. Model-checking one critical component costs a week. A proof from specification to implementation costs what seL4 cost.

Five materials, five prices, five strengths. The engineering question is which one this load needs, not which is most impressive. Most projects that would benefit from the third rung reach for the first or the fifth, and the fifth is where the field acquired its reputation for costing more than it returns. Reaching for full proof when a type would have done is not rigour, it is the same category error as building a shed in structural steel.

Use mud when one person holds the whole interaction surface, the lifetime is short, and being wrong is cheap and reversible. Asking a model to draft a reply to an email is a mud hut and should be. It has no n, nobody is underneath it, and building it in steel would be an absurdity.

Reach for steel when n has grown past the crossing, when the artefact will outlive everyone's memory of writing it, and when a contradiction costs something other than an afternoon. A commercial contract drafted from scratch. A product with a hundred requirements that must all hold at once. A policy a regulator will read adversarially, years from now, looking for exactly the pair you did not check.

For those, prose is not lazy. It is a material with a published height limit, and you are proposing to build well above it.

What exists today, plainly

Every essay in this series carries this section, because the field describes its destination in the present tense.

The mechanism is real and I run it daily: requirements as schema-valid data, the load-bearing ones modelled as decidable predicates in Lean 4, and a gate that refuses to let a written claim assert as proven anything the kernel has not checked.

I would like to tell you it has caught contradictions of exactly the R1-and-R2 shape, because it has. But notice that this is an anecdote about work you cannot inspect, from someone with an obvious interest in the conclusion, and the specifics sit inside engagements I will not publish. Weight it barely. The argument here is combinatorial and stands on its own; if it needed my testimony it would already be in trouble.

Nor is any of it finished. My own libraries carry real proof debt: open obligations, standing axioms, and at least one invariant that turned out false as stated and needed restating rather than proving. The verification harness exists partly to stop me quoting a rounded total that flatters the position. Anyone selling a completed formal stack is selling something else.

The height limit of mud is a fact about mud. The datasheet for the replacement is still being written, and some entries currently say unknown.

The load, not the material

The engineer's question is never "is this a good material". It is "what is the load, and what happens to the people underneath when it fails".

Answer that first and the choice of material stops being taste and becomes a calculation, which is the whole of the discipline.

Part two, The Gun Did Not Win, asks which countries can absorb this. Part three, Make the Safe Harbour Compile, asks what regulators should do with it.

The mechanism sketched here is worked through in When the Spec Can Contradict Itself; the schema layer beneath it is in Requirements as Data.

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.