Where This Book Is Wrong

The Verifiable Trace essay said of a law firm's article, for about seven months until I corrected it in November 2026: "The phrase 'clearly documented legal grounds' is doing a lot of work here." The article does not contain that phrase. An audit of seventeen of my older essays, whose corrections went into this book on 02/11/2026, found nine rows like that one in that essay alone: paraphrases printed inside quotation marks and attributed to a named firm. A text search of the article would have found every one. The search was available when I published. I did not run it, and no technology was missing.

Thesis. The book survives as an account of what makes automated work defensible, and fails as a forecast of what gets bought. Four verdicts follow. Checkability is not the constraint binding law firms today: liability allocation is, and a firm buys no check whose avoided loss falls wholly on somebody else, until a regulator, insurer or client moves some of it back. Formalisation is regressive here, and the book has no costed answer. The formal layer floats by the test of Floating Theories: it checks the book's interior, and no theorem in it is about a running agent. And self-interest has bent my emphasis and my statements about my own systems. The most contestable claim is the first. Most chapters argue as if better evidence would create its own demand. If firms start paying for machine-checked evidence with no change in who bears the loss, I am wrong and the book is stronger than I say.

I build AI systems for law firms and I sell the discipline this book recommends, so a counter-chapter that leaves the sale standing is itself a sales device.

What the audit found

Each row of the corrections files gives the old sentence, the source and the replacement. Class A means contradicted by a source. Class B means it cannot be sourced. Class C flags a name for a decision and is not an error.

So 97 of 283 audited statements were wrong or unsourced. That is not a rate per sentence, because the files record claims chosen for checking. The six merged essays add 56 rows from a narrower check, with no comparable denominator. The book holds 20 existing essays, and only eleven of those have a corrections file today.

Unsourced quotation. The nine rows above. The article said something close each time, so the replacements are verbatim and the argument mostly stands. An essay about what a claim rests on printed words its source never used, then commented on the wording.

Code claims in the wrong tense. "The verification infrastructure is production-grade" is now cut: the public repository had no continuous integration at that date, and its own review record quotes a reviewer calling a sorry gap "fatal to the practical deployment claim". The same essay said that ClawCombinator's data lifecycle was enforced "at the infrastructure level". The replacement says: "None of this is implemented." Nine rows of that essay claim things the audit could not find.

The honesty device failed. A passage headed "What exists today" said "The automatic enforcement is operational". This book asks every chapter for such a passage, and here the passage was the false part. A label in prose checks nothing.

Errors in the discipline itself. When the Spec Can Contradict Itself told readers how to detect a vacuous predicate and had it backwards, and its first code block failed as printed while the essay said the modelling "is real and runs". Requirements as Data called owner the single most valuable constraint, and my own schema does not require it: 188 of 2,068 requirements carry one.

Numbers with no source. "a few thousand annotators", where the one figure I could check is about 40. Law firms shedding juniors, "observable in practice", with no data. A "Grade A" that the NICE manual chapter I read does not contain.

Not every error flattered me. The essays said LegalLean had 87 theorems when a count of the public source at that date gives 92 proved. Nine rows of overclaim in one essay against one understated count is still a direction, and it points at what I sell.

Four essays in this book say in print how they were made: two "started as a conversation with an AI research assistant", and two say "Written with my AI research partner". Those last two were audited and took 18 class A or B rows between them. The corrections files do not say who or what produced each error, and I do not attribute them. I published them, and where an assistant helped, that is the book's own premise showing up in the book's own defects.

Challenge one: checking may not be the bottleneck

The book's sentence is that once generation is cheap, checking becomes the scarce thing.

Checking a legal citation means looking it up. Damien Charlotin's database listed 2,252 decisions on 02/11/2026 in which a court or tribunal found or implied reliance on hallucinated material (Charlotin, read 02/11/2026). It counts only what was caught, across jurisdictions. By my sum of its party chart, about 40% came from lawyers and most of the rest from litigants in person. For the lawyers, no capability was missing. A preregistered study found that legal research tools from LexisNexis and Thomson Reuters each hallucinated "between 17% and 33% of the time" (Magesh et al., 2025; I read the arXiv abstract), on 2024 versions. In Thomson Reuters' survey of more than 1,500 professionals, a vendor's survey, a corporate counsel explains what outside firms are relied on for: "I trust them to make the right decisions and stand behind their advice wherever it comes from" (Thomson Reuters Institute, 2026). That sentence asks who stands behind the work, not for evidence.

The money is moving on liability and is not asking for proofs. Where it does ask for evidence it asks as the party carrying the loss: AIUC sells audit and insurance together, on a standard "Grounded in technical testing" (AIUC-1). In the United States, Verisk's general liability forms effective January 2026 let insurers "generally exclude this emerging exposure" (Independent Insurance Agents, reporting Verisk). That is not solicitors' professional indemnity. In England and Wales the compulsory layer "must not exclude or limit the liability of the insurer" beyond a closed list (SRA minimum terms, clause 6), so Verisk's move is not open there, and I have not surveyed wordings elsewhere. In England and Wales, the Divisional Court in Ayinde looks to managing partners, as The Last Person Who Knows How reports. Madeleine Elish named the human end of this: a person in a complex automated system can become "simply a component" bearing "the brunt of the moral and legal responsibilities" (Elish, 2019). Partners already are that component. A signature costs less than a proof, and courts and insurers already know how to read one.

The older version of this attack came long before AI. In 1979 De Millo, Lipton and Perlis wrote that "it is a social process that determines whether mathematicians feel confident about a theorem", and that because no comparable process exists among verifiers, "program verification is bound to fail" (De Millo et al., 1979). In 1996 Hoare asked how software got so reliable without proof, and answered that the means were review, targeted testing and over-engineering, with "Formal methods and proof play a small direct role in large scale programming" (Hoare, 1996).

Against all that, three things. The same Thomson Reuters report lists "Reliability/accuracy concerns" first among reasons professionals give against using these tools, so the market does say it cares. De Millo's social process now exists for one kind of formal artefact: Mathlib has reviewers, and the review queue is what it reports as its constraint, as Who Pays to Keep It True? quotes. And agents formalised Fermat with a kernel in the loop (Mathematics Went First).

Verdict: the book's sentence survives as a statement about cost and fails as a statement about demand. Formal checking is what is expensive if you want it. It is not what law firms are short of wanting. The formal version takes one line. In lean/BuildingInSteel/CounterChapter.lean, the definition buys assumes a buyer pays only when the cost is below its own share of the avoided loss. On that assumption no_share_no_purchase proves that a buyer bearing none of the loss buys no check, at any cost and any size of loss, and full_share_buys proves that a buyer bearing all of it buys any check cheaper than the loss. Both restate the assumption and do not test it. Its inputs are parameters, and I hold no value for any of them.

So the most useful chapters are not those that make checking cheaper. They are A Proof Is Not an Appeal and Perfect Compliance, Defeated Purpose, which ask who carries what. My own first exhibit tests buys. Charlotin's lawyers risked sanction and a lookup cost almost nothing, so on buys they should have checked. A share of the loss is therefore necessary and not sufficient: the loss must also look likely to the person choosing. I would give this verdict up on seeing firms pay for machine-checked evidence with no regulatory, insurance or client requirement behind it.

Challenge two: what formalising costs, and who pays

A Proof Is Not an Appeal says a Lean certificate "is unreadable to almost everyone it could be used against". Catala, the best method in this field, took 50 hours of pair programming for one benefit, as The Translator Writes the Rule records. The Last Person Who Knows How prices its drill at 120 unbilled hours for an invented group of 20. Who Pays proposes a fee and concedes it favours large firms. Disclosure Without a Predicate says a public check "would also favour firms able to pay for a register, and I sell to those firms".

The book has no costed answer to any of these. James C. Scott's question is whose knowledge disappears when a practice is made legible (Scott, Seeing Like a State). I read the publisher's page and not the book for this sentence, so take it as my use of a familiar argument. The partner who objects on instinct and the junior who learned by doing the work have no field in any schema here.

Each chapter carries a required paragraph on what formalising loses, and required paragraphs turn into ritual. I can name places where the loss changed the design: Perfect Compliance narrows its presumption to evidence close to the purpose, and The Last Person drops Lean altogether. In most chapters the loss is stated and the recommendation stands unchanged.

Verdict: the book fails here and should say so. Its proposals are regressive as written. The defence I will still make is the one in How High Can You Build in Mud?: "most software should be a mud hut". The book is defensible only for high-consequence work, by firms that can afford it, and everyone else should ignore it without guilt. I would change my mind on seeing a small firm or a legal aid practice run any proposal here at a cost it reported as worthwhile.

Challenge three: Floating Theories, applied to this book

That essay defines a floating theory as claims securely connected to their premises and not anchored to the domain, and separates four roots: premises, interpretation, observation and cause. It claims that "a green proof raises the credibility of the whole structure while checking only its interior".

Interpretation floats. Before this chapter the book's 15 Lean files held 436 theorems in 7,075 lines, by a grep for theorem at the start of a line, and 111 lines end in := by decide. They are about the Ashdown instruction, a case the book invented, and about small models. No theorem is about a running agent system. The chapters say so one by one, and "kernel-checked" still appears throughout. Floating Theories predicts a badge effect in an experiment with lawyers. This book is a candidate for its treatment arm.

Delete the Lean and ask what falls. The chapters answer for me: "twenty lines of Python would do it" and "conceded" (A Summary Is Not a Permission), "You do not need Lean to get most of the value" (Never Breaks a Rule, Never Finishes), "no firm needs Lean for this" (Disclosure). Two proofs are "two cases, because all the content is in the type". What the Lean did do is catch me: Grant.narrows ignoring revocation, a first gate that over-refused, a siblings encoding that looks neutral and is not. So I hold this: the Lean's main value in this book is as a discipline for its author, and readers should give "kernel-checked" no extra weight for any claim about the world.

Observation floats where it matters most. Thirteen proposals in these chapters have not been run: the release manifest, the handover slice, the translation gate, signed scope notes, the sunset presumption, the capability language, the root-issuance log, the two-job memory gate, the run evidence manifest, the tier rule, the appeal packet, the intervention drill and the corpus levy. Each chapter says so about itself. That is honest, and it means the book reports no measured effect of its own remedies.

Cause is contested. Mud says of formal methods that "they lost on price", and "The bill got smaller." I gave no source for the cause. Hoare's paper supports a rival: they lost because other methods were good enough. If Hoare is right, a smaller bill changes little.

Premises hold best. Generation did get cheap, and review capacity did become a reported constraint, in Mathlib, the one project where I read a good measurement of it.

Verdict: the structure floats, and the empirical passages do not. The theorems add precision to definitions and no evidence about the world. Where the book holds weight, it is on sources read, and the audit shows how that fails too.

Challenge four: the author sells this

Chapter after chapter discloses. In six experiments Sah, Loewenstein and Cain found that disclosure "can decrease advisees' trust in the advice" and "can also increase pressure to comply with that advice", and that this pressure falls when disclosure comes from "an external source rather than from the advisor" (Sah et al., 2013). Those were advisees in experiments, not readers of a book, but it removes the comfort that a disclosure clause does the job.

Look for the distortion where facts run out. Eight other chapters have a Thursday section asking a partner for something small. All eight are reasonable, none tells a partner to stop using a tool, and all raise the salience of what I sell. The book's rankings mostly put checking first. The Elan page still says, as I read it on 02/11/2026, "FINRA / SEC / SOC2 Ready" and "SRA / ABA / IRAP / EU AI Act Ready", and it still says of its chain "proved in Lean 4", which A Trace Is Not a Replay shows is a theorem that claims nothing. I have not audited those compliance modules, and that is the point: a page making those claims under my name is on the wrong side of this book's own standard.

Verdict: guilty on emphasis and on my own products, not shown on the general argument. The theorems do not care who sells what, and the citations can be checked. Discount every ordering and every statement about what exists in my own systems. A partner should read this book as an argument by a vendor.

A rule I published: does Elan's min fall to sybils?

The page says confidence is "propagated as min(own, min(deps))", so that it "degrades monotonically along dependency chains", and names a top band, "Verified", at 0.95 and above, described as "declarative, machine-checkable". The critique I set out to test says a sybil attack [one party posing as many, in Douceur's sense] amplifies false confidence through correlated copies.

The narrow critique is false. This compiles, from CounterChapter.lean; the statements are copied and the proofs are in the file.

theorem adding_never_raises (own d : Nat) (deps : List Nat) :
    conf own (d :: deps) ≤ conf own deps :=

theorem copy_changes_nothing (own d : Nat) (deps : List Nat) (h : d ∈ deps) :
    conf own (d :: deps) = conf own deps := by

Both are general. many_copies_same extends the second to any number of copies. A rule that counts agreement does fall to copies (counting_rule_is_sybil, computed). A rule that counts distinct sources resists copies under one name (dedupe_resists_copies) and falls to one new name per copy (relabel_defeats_dedupe, computed), which is the attack John Douceur named. His result, for peer-to-peer systems, is that without "a logically centralized authority, Sybil attacks are always possible" except under "extreme and unrealistic assumptions" (Douceur, 2002). min counts nothing, so it has no identities to forge.

The broad critique holds, and it is not about min. correlated_all_wrong_verified computes three inputs from one source, all wrong, reaching the top band. no_score_of_reports_separates shows that any function of the reported numbers gives one answer for those and for three independent right inputs at the same scores. It is general over the function and fixed on those two lists. min is not guilty of this, and no replacement arithmetic would fix it. Correlation has to be an input.

The direction of the risk is the reverse of the usual reading. Correlation looks like min's weakness. If scores are probabilities, it is where min is right.

theorem joint_le_each {W : Type} (ws : List W) (ps : List (W → Bool)) (p : W → Bool)
    (h : p ∈ ps) : count ws (allHold ps) ≤ count ws p := by

That is the upper half of the Fréchet bound (Wikipedia's statement, which I used as a lead), in counts over a finite space, compiling from the same file. The chance that every input holds is at most the chance of each, however they correlate, so min is a ceiling on the joint and not a floor. comonotone_exact computes two perfectly correlated inputs at 90: joint 90, and min is exact. independent_overstated computes two independent inputs at 90: joint 81, and min still says 90. So a rule whose page says confidence "degrades" degrades too little in precisely the independent case, and a second opinion at the same score earns nothing (independent_second_opinion_earns_nothing), though independent checking is what The Checking Threshold says is worth having. Read the score as possibility theory's necessity instead, where N(U ∩ V) = min(N(U), N(V)) by the reference statement I read, and min is correct by definition, and "Verified" then says nothing about how often it is right. Belief-function theory reached for the same property on purpose: Denœux's cautious rule is idempotent [gives the same result when combined with itself], which "makes it suitable to combine belief functions induced by reliable, but possibly overlapping bodies of evidence" (Denœux, 2008). So this is a recognised design, and my page says neither which reading it means nor why.

One input decides. one_low_input_decides is general: add one input and the output is at most that input. Copies cannot push the score up, and whoever can add one low dependency can push it down to a band that blocks a run. The sybil risk runs in reverse, as denial.

What feeds it is the real finding. The function is in a private repository and the adapter in a public one. I describe both and quote neither, and I read them on 02/11/2026. The function that propagates min along dependencies exists in a sister repository. My search of the repositories under the same parent found no caller, tests included. What the benchmark adapter does is take three numbers and classify their minimum. Two are chosen by whether a text passes a length threshold. The third is a constant that ignores what the verifying step returned. adapter_three_values, proved over my own description of that shape and checked against no running code, shows the result is always 65, 70 or 85. The "Verified" band cannot be reached on that path, and neither can the band the page says blocks synthesis. A separate textual gate can halt the run, and the confidence band cannot. So the score does not measure what its name says, and sybils are beside the point: on this path you do not need to forge an identity to get a good score, only to return a long enough string that the textual gate lets through.

Verdict. Sybil amplification, as stated, does not hold. Correlated inputs can all be wrong at a high score, as the critique says, for a reason that indicts every score of reported numbers. And the rule as wired has a worse problem than either. The correct version is the manifest in The Proof Passed. The Wrong Thing Ran.: a typed basis naming who checked what against which digest, with no number calling itself "Verified". I would reverse this if a held-out test of seeded errors showed those bands predicting correctness, which the fourth prediction below expects it will not.

The chapters I expect to fail

The chapter I would bet on is A Trace Is Not a Replay: its split is definitional, it corrects something specific, and its one contested sentence has a clear test.

What the predictions are worth

Goodhart applies to the book's own ledger. Of the 43 predictions in the 15 chapters written for this book so far, 23 by my reading say that an institution will not have done something by a date, 16 say something will happen, and 4 mix the two. Standards bodies and regulators are slow, so most of the 23 win by default. A book that scores itself on the total will look prescient and have learned little. So The Predictions Ledger should score the two kinds apart, and I give that as the second prediction below.

What exists and what is proposed

Proved generally, in CounterChapter.lean (21 theorems, no sorry, no declared axioms; #print axioms lists at most propext and Quot.sound on those it prints): adding_never_raises, copy_changes_nothing, many_copies_same, one_low_input_decides, joint_le_each, no_share_no_purchase, full_share_buys, independent_second_opinion_earns_nothing. General over the function, on two fixed lists: no_score_of_reports_separates. General over two Booleans, about my description of the code and not the code: adapter_three_values. Computed on fixed values: correlated_all_wrong_verified, counting_rule_is_sybil, dedupe_resists_copies, relabel_defeats_dedupe, comonotone_exact, independent_overstated, worth_it_not_bought.

Measured: the audit counts, the Lean counts and the prediction split, the last by my own reading. Sketched: that liability allocation is the binding constraint, for which I have illustrations and no measurement across firms. Proposed: an outside audit of the new chapters, and scoring predictions by kind. Not done: a survey of professional indemnity wordings, any test of the Elan bands, and audits of the other 9 existing essays.

Objections to this chapter

"Confession is the sale. A vendor who publishes his errors buys trust cheaply." Verdict: accepted, and I have no defence from inside the text. A list of errors the author chose to publish is weaker evidence than one he could not stop. What would change my mind is an independent audit finding little that I missed, which would make this chapter more than theatre. The third prediction bets against that.

"You chose your attackers. The real objection is that a system smarter than its checker routes around all of this." The agents in OpenAI's report, as The Hands records, found zero-days in a mediator, and a generator could write statements its reviewers wrongly accept. The book's small trusted checker assumes a statement someone can read. Verdict: accepted as a limit. This book is about engineering and law over the next few years, and it does not offer a solution to alignment. I would change my mind about its usefulness if reviewers measurably stopped catching what strong generators write.

"joint_le_each is first-year probability, and you dressed up a one-line fact." Verdict: conceded on novelty. It earns its place because the page it corrects carries my name and got this wrong. I would cut it if that page changed.

Goodhart, and what is lost

Publish an error count and the cheapest way to lower it is to audit less, so the number to watch is claims audited and who chose them. Replacing a confidence number with a typed basis loses something as well: a rough score is quick to read, and a tired reviewer will use it whatever it means.

What to do on Thursday

If you are a partner, I am not asking you to code, buy anything or change how you practise. Ten minutes. Next time anyone sells you an AI system, me included, ask two things in writing.

1. Name one public claim you have withdrawn about your own product in the last year, and show where.
2. If this system's error costs a client money, who pays, under which clause and which policy?

"We have never had to withdraw anything" is the finding. The second answer tells you whether anyone on their side has a reason to check. It may also tell you that you are the one paying and the one checking, which is close to where Ayinde put managing partners on 06/06/2025. The external date is your next policy renewal, when your insurer may ask you the same question.

Predictions

1. By 31/12/2028, at least one professional indemnity insurer publishing wording for solicitors in Australia, or for the layer above the SRA's compulsory minimum in England and Wales, will add an express AI exclusion or condition, and no such condition will name machine-checked evidence. Refuted if none appears, or if one names it. If this holds, liability moved first and checking was not what it asked for.
2. On 31/12/2028, at least 80% of the 23 no-change predictions counted above will stand confirmed, and fewer than half of the 16 change predictions will. Refuted by either figure failing. Voids count as unconfirmed.
3. By 31/12/2027, an audit of at least five of the new chapters, by someone with no stake in the book, will produce at least ten class A corrections. Refuted by a published audit finding fewer. Void if none is done, which would itself be a finding about who wants this checked.
4. If the benchmark adapter's bands are tested on a held-out question set by 31/12/2027, the share of wrong answers in the second-highest band will be within ten percentage points of the share of right answers in it. Refuted by a wider gap. Void if the test is not run.

The book's claim is smaller than it looks, and I think it holds. Where a person will have to defend what a machine did, these are the distinctions to have. Nothing in it shows that anyone will pay to have them until the bill for lacking them reaches the person choosing.

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.