Floating Theories

Some aquatic plants grow roots that do not reach the bottom. In the floating species of Ludwigia, once filed under Jussiaea, the stems lying on the water put out white, spongy roots, which the Flora of North America describes as roots "that facilitate aeration needed for root respiration" (Flora of North America, Ludwigia). Duckweed and frogbit simply hang their roots in the water column. A free-floating plant like these is whole, alive and well connected: every leaf joined to a stem, every stem joined to the rest. What it is not is anchored. It goes where the water goes. Ludwigia is the subtler case: its stems often root where they touch the mud, while the white roots on its floating stretches anchor nothing.

I have started using that picture for a failure I keep meeting in formal methods, in medicine, in organisations and, more and more, in what AI systems produce, and I want to give it a name with an explicit definition, because the rest of this essay argues that names without definitions are part of the problem:

A floating theory is a body of claims whose conclusions are securely connected to its premises, but whose premises, or whose interpretation, are not anchored to the domain it claims to describe.

The argument of this essay is that proof and anchorage are separate obligations, that a well-made label can pass for anchorage when it is only a description, and that the combination of AI and formal verification is about to make floating theories both cheaper to produce and harder to spot. The last claim is the one I think would most surprise a sympathetic reader, so I will state it now in a form that could be wrong: a green proof raises the credibility of the whole structure while checking only its interior, so verification used without a separate anchorage check makes floating theories more persuasive, not less.

I should say up front that I build AI systems for law firms and use formal verification to do it, so I have an interest in people trusting proofs. This essay argues for trusting them less than a badge invites, which cuts against that interest. I have tried to cite the evidence where it is uncomfortable for me, to name the prior work that got here first, and to end with predictions that could prove me wrong.

This essay started as a conversation with an AI research assistant, and I have treated that conversation as data, not as a source. Every factual claim below was checked against the primary paper, the guideline or the reference manual, and the record of that checking sits beside the draft. One small example of why that matters: the assistant described the floating roots of Jussiaea as specialised flotation structures that also help with respiration. The botanical flora I checked describes them as organs of aeration and says nothing about flotation. The plant was fine. The sentence about it was floating.

What a proof secures, and what it does not

Here is a theorem in Lean, the proof assistant I use most. It compiles on Lean 4.29.1.

theorem eligible_of_verified (Verified Eligible : Prop)
    (policy : Verified → Eligible) (verified : Verified) : Eligible :=
  policy verified

It says that if verification implies eligibility, and verification holds, then eligibility holds. Lean checks that, and the check is as good as checks get. What Lean does not check is whether policy is the policy that actually governs anyone, whether anyone was actually verified, or whether the words Verified and Eligible mean what a lawyer, a regulator or an applicant would mean by them. The stems are joined. The roots dangle.

That is not a flaw in the proof. It is a conditional statement doing exactly what conditional statements do. The defect, when there is one, is in how the result is presented: as if the theorem had established eligibility, rather than established that eligibility follows from two things nobody has yet shown.

Lean's own reference manual is plain about where its guarantee stops. On axioms, which are statements a user asserts without proof, it says: "By their very nature, Lean cannot check whether new axioms are consistent; please exercise care when adding axioms," and it describes #print axioms, which lists every axiom a theorem depends on, as a way "to audit the assumptions made by a proof" (Lean Language Reference, "Axioms"). An earlier essay on this site, How High Can You Build in Mud?, was about the loud version of the failure, in which contradictory axioms leave the build green. This one is about the quiet version, in which the axioms are perfectly consistent and simply not true of anything in particular.

The quiet version has a visible form and a hidden one, and the difference matters in practice. Put the same rule in as an axiom instead of a hypothesis:

axiom Applicant : Type
axiom Verified' : Applicant → Prop
axiom Eligible' : Applicant → Prop
axiom policy' : ∀ a, Verified' a → Eligible' a

theorem eligible' (a : Applicant) (h : Verified' a) : Eligible' a :=
  policy' a h

#print axioms eligible_of_verified
#print axioms eligible'

Run together as one file, both blocks compile on Lean 4.29.1. Lean reports that the first theorem "does not depend on any axioms" and that the second depends on Applicant, Eligible', Verified' and policy'. In the first version the dangling root is printed in the theorem's own type, where every reader sees it. In the second it has been moved into the environment, where only someone who runs the audit will find it. Both are floating. Only one of them admits it on its face.

There is a third form, and it is the hardest to catch, because it passes every audit. Suppose the rule says that applicants aged 18 or over are eligible:

def Eligible'' (age : Nat) : Prop := age > 18

theorem eighteen_ineligible : ¬ Eligible'' 18 := Nat.lt_irrefl 18

#print axioms eighteen_ineligible

This also compiles, and Lean reports that eighteen_ineligible "does not depend on any axioms". Nothing is assumed, nothing is vacuous, and the theorem is a true fact about the definition. The definition is simply wrong: it turns away every applicant on their eighteenth birthday. No audit of assumptions can catch a definition that means the wrong thing, because the wrong meaning is not an assumption. It is the content.

I know a cruder relative of this form from my own work. In June this year an adversarial check of a generator I had built, which turned product requirements into Lean specifications, found that it had formalised acceptance criteria as the proposition True: 588 of them in the largest single specification, and the same pattern in every specification it had produced, together with a legal authority copied in from the generator's default into documents where it had no business. Every file type-checked. None of them proved anything about the requirements they were named after. The build was green because there was nothing in it to fail. What found it was not the build but a second AI agent whose only instruction was to refute each specification against the prose it claimed to formalise. That was the easy case: a specification of True can be caught by pattern, and a lint that fails any new one now runs on every commit at negligible cost. The hard case, a specification that says something definite and wrong, like the one above, has no pattern to lint for. The only checks for it are a person who knows the domain reading it back, or a test against cases whose answer is already known, and those are the checks that cost time.

Four roots, not one

"Grounded" is too blunt a word for what is missing, because a claim can be anchored in one respect and adrift in another. I find it useful to separate four roots, each of which can reach the bed or fail to independently of the others.

The proof is none of these. It is the stem that joins premises to conclusion. That is why a kernel-checked theorem can be impeccable while three of its four roots hang in open water.

Two pieces of evidence show how much weight the interpretation root carries even among people who formalise for a living. The first is the cleanest measurement I know of the boundary of a proof's guarantee. Xuejun Yang and colleagues used Csmith, their generator of random C programs, to hunt for compiler bugs, and found wrong-code errors in every compiler they tested. CompCert, the formally verified compiler, was the instructive case. Its early version had six silent wrong-code bugs, all in the front end that had not yet been verified, and partly in response its developer extended the verified portion. Two more problems came from a different place: CompCert's formal model of the PowerPC processor "failed to specify a constraint on the width of this immediate value, on the assumption that the assembler would catch out-of-range values". In those cases the assembler did catch them: an unverified tool that the model's authors had relied on to check, and that did. The proof was correct about a model of the processor that was not quite the processor. After that, and about six CPU-years spent trying, they could find no wrong-code errors in the early-2011 development version, and "the middle-end bugs we found in all other compilers are absent" (Yang, Chen, Eide and Regehr, 2011, PLDI, 283-294). The proof held exactly where it was anchored. Where the model of the world was wrong, testing against the world is what found it.

The seL4 team, who produced the first machine-checked proof of functional correctness for a general-purpose operating-system kernel, made the same boundary explicit from the start: the proof assumes the correctness of the compiler, the assembly code, the hardware, the cache and TLB management and the boot code (Klein et al., 2009, SOSP, 207-220), and the project still publishes its assumptions as a list (seL4, "Verification assumptions"). That list is what anchorage looks like when someone takes it seriously. It is a statement of which roots reach the bed, and which are held by trust. It has also got shorter. Translation validation later removed the compiler from the trusted base on some architectures, so that the proof now reaches the binary code (Sewell, Myreen and Klein, 2013, PLDI, 471-482). A root that had been held by trust was lowered to the bed.

The second is more recent. miniF2F is one of the standard benchmarks for AI theorem proving in Lean: competition mathematics problems, each written in English and in Lean. An audit published last year found discrepancies between the formal and the informal statement in more than half of its problems. On their corrected version, the best reported accuracy rose from about 40% to 70% (Ospanov, Farnia and Yousefzadeh, 2025, arXiv:2511.03108). Read that slowly. The original formal statements were written by people, and for years published results reported machine-checked proofs of statements that, in many cases, were simpler than, or different from, the problems they were labelled as. Every one of those proofs was correct. The checks that did happen were piecemeal, a handful of statements fixed here and there, until someone compared every statement with its source.

The same paper has a second finding, closer to what AI is now doing. The authors had AI systems translate the English problems into Lean, then compared two ways of checking the translations: an automated judge built on a language model, and a human who reads Lean. When each translator made 128 attempts per problem and the judge chose among them, it rated 97.5% of one translator's statements on the original test set correct where the human rated 62.7%; for a second translator the figures were 98.4% and 90.6%. With a single attempt the pattern reversed, and the judge was stricter than the human. Either way, a model's verdict on a model's reading was no stand-in for a person's, and it was most generous exactly when it was being used to pick the model's own output.

Colic: anchored to what?

The plant picture breaks in an instructive place, and medicine is where it breaks.

"Colic" sounds like a diagnosis. The NHS describes it as "when a baby cries a lot but there's no obvious cause", and says "it's not known exactly what causes some babies to get colic" (NHS, "Colic"). It has had operational criteria for more than seventy years. Morris Wessel and colleagues' "rule of threes" defined it as paroxysms of fussing or crying lasting more than three hours a day, on more than three days in a week, for more than three weeks, in an otherwise healthy infant; the paper's title, "Paroxysmal fussing in infancy, sometimes called 'colic'", already keeps the word at arm's length (Wessel et al., 1954, Pediatrics 14(5), 421-435). The Rome IV criteria later dropped the three-hour threshold from the clinical definition, which now turns on recurrent, prolonged crying or fussing without obvious cause that caregivers cannot prevent or resolve, and kept a three-hour threshold, confirmed by a diary, for research (Benninga et al., 2016, Gastroenterology 150(6), 1443-1455).

So colic is not a floating theory in the sense I defined. Its observation root reaches the bed: the crying is real, observed and measured by stated criteria. It is its cause root that dangles. The precise way to say it is that colic is observationally anchored and causally underdetermined. It is a description, and a useful one, wearing the grammar of an explanation.

Gastro-oesophageal reflux looks like the opposite case, because it names a mechanism: stomach contents coming back up into the oesophagus. But having a mechanism available does not anchor it to a particular baby's distress. Three separate claims are easy to fuse into one:

1. Reflux occurs in this baby.
2. Reflux is causing this baby's distress.
3. Suppressing acid will relieve this baby's distress.

The first can be observed. The third was tested directly. In a multicentre, double-blind trial, 162 infants whose symptoms had been attributed to reflux were randomised to the proton pump inhibitor lansoprazole or to placebo for four weeks. The response rate was identical, 54% in each group, and serious adverse events, particularly lower respiratory tract infections, were more frequent on the drug (Orenstein et al., 2009, Journal of Pediatrics 154(4), 514-520). The joint North American and European guideline now says plainly: "The working group recommends not to use H2RA or PPI for the treatment of crying/distress in otherwise healthy infants" (Rosen et al., 2018, Journal of Pediatric Gastroenterology and Nutrition 66(3), 516-554).

I am not giving medical advice, and nothing here is about any particular child. The point is structural. The mechanism-shaped word did a kind of damage the description-shaped one could not, because it supplied a treatment, and the treatment rested on the second claim in that list, which is the one nobody had anchored. And notice what anchored the third claim in the end: not a mechanism, but a randomised trial. Causal evidence can arrive before anyone understands the mechanism, and it is worth more than a mechanism that has not been shown to operate.

The nominal fallacy

The trap in both cases has a name, and an old joke attached to it. In the final interlude of Molière's Le Malade imaginaire (1673), a candidate for a medical degree is asked why opium makes people sleep. He answers, in dog Latin, quia est in eo virtus dormitiva: because there is in it a dormitive virtue, whose nature is to make the senses drowsy. The examiners applaud. The answer has the form of an explanation and the content of a repetition.

Stuart Firestein calls this the nominal fallacy, "the error of believing that the label carries explanatory information" (Firestein, 2011, "The Name Game", Edge; see also Ignorance: How It Drives Science, Oxford University Press, 2012). His examples are words like "instinct", which name behaviour without saying what produces it. The conversation I started from produced a shorter version that I now use as a rule: treat labels as compression, not explanation. A good label compresses a set of observations and criteria. It becomes a fallacy at the moment it is used to answer "why?".

AI has its own dormitive virtues, and the most instructive is "emergence". For a while, the observation that large language models suddenly acquire abilities at some scale was widely reported, and "emergent abilities" was often used as though it named something the models did. Rylan Schaeffer, Brando Miranda and Sanmi Koyejo showed that many of these apparent jumps were produced by the choice of metric: nonlinear or discontinuous scoring turns smooth improvement into an apparent leap, and continuous metrics make most of the leaps disappear (Schaeffer, Miranda and Koyejo, 2023, "Are Emergent Abilities of Large Language Models a Mirage?", NeurIPS). Their result does not show that no abrupt change can ever happen. It shows something worse for the label: the observation root itself had been partly made by the measuring instrument. The word had been explaining a pattern that was, in many cases, an artefact of how the pattern was measured.

Organisations are full of the same move. "It's the culture" is offered as the reason a change failed. "Alignment" is offered as the thing a team lacks. Each is sometimes a fair summary and often a dormitive virtue.

Applying it to my own term

Two days ago I published Systemic Coping Syndrome, which coins a clinical-sounding label for an organisational pattern. It would be dishonest to write this essay without running that term through the same four roots, so here is the audit.

By its own admission, then, systemic coping syndrome is closer to a floating theory than to colic. Colic's observation root reaches the bed and only its cause root dangles; my term has a definition and a mechanism but no measurement yet. What keeps it on the right side of the nominal fallacy is not that it is anchored. It is that the essay says which roots are missing, does not offer the label as the reason anything happens, and lowers the two missing roots, observation and cause, towards the bed in the form of three predictions with measures, baselines and horizons. If those predictions fail, the term should be retired. I would rather say that now, in public, than have someone else find the dangling roots for me.

The general lesson is the one I most want to keep: coining a term is not the error. Presenting it as more anchored than it is, is.

Why AI makes floating theories cheaper and more persuasive

Now put the two halves together.

A large language model is trained to produce text that is plausible as a continuation, tuned to produce answers people prefer, and increasingly trained against automatic checkers: answer keys and test suites (Guo et al., 2025, Nature 645, 633-638), and proof assistants (Hubert et al., 2025, Nature 651, 607-613). The first two reward fluency. Answer keys and test suites do reward a narrow kind of anchorage: they are cases whose right answer is already known, which is remedy 3 below, though they anchor only the final answer. A proof checker does not. It accepts any correct proof of whatever statement it is handed, so training against it rewards the stems by construction and is silent about the roots. Internal coherence, a confident register and the right vocabulary are all things such a system does well, and they are exactly the properties of a well-connected plant with nothing under it. I do not claim that models cannot be grounded: retrieval, tools and checking all add roots. I claim that fluency is the default and anchorage is the add-on, which is the reverse of what a reader's instincts assume about polished prose.

Formal verification is the obvious antidote, and I spend much of my working life arguing for it. But it fixes the stems, not the roots. When an AI system writes the formal statement and an AI system proves it, the kernel will certify the connection between them with a reliability that no other kind of evidence approaches. The kernel, together with anything a proof tells it to trust, is itself a root held by trust, but it is a small and much-inspected one. The roots that matter here are the statement's, and the miniF2F audit shows what happens to them when nobody checks them separately: formal and informal statements disagreed in more than half of the problems, under correct proofs, for years.

That leads to the claim I stated at the start. A proof is unusual among forms of evidence in that it is binary and nearly incontestable. Its credibility does not stay where it was earned. A reader who sees "formally verified" next to a set of rules is unlikely to separate the part of the claim the kernel checked, that the conclusions follow, from the part it did not, that the rules are the right rules. Something close to it has been measured twice. People supervising an automated aid miss errors that the aid does not flag (Skitka, Mosier and Burdick, 1999, International Journal of Human-Computer Studies 51(5), 991-1006), and non-experts find bad explanations more satisfying when irrelevant neuroscience is attached, which in that study's words masks "otherwise salient problems" (Weisberg et al., 2008, Journal of Cognitive Neuroscience 20(3), 470-477). I have not seen it measured for proof, and for proof it is a hypothesis, not a finding; but if it is right, verification without an anchorage check does more than fail to help. It lends the authority of the stems to the roots.

What exists and what does not

• What exists: the studies, guidelines and reference documentation cited above, each of which measured or stated what it says. The three Lean blocks, run together as one file, compile on Lean 4.29.1, and the #print axioms output quoted is what they produce. The True placeholders, 588 in the largest single specification and the same pattern in every other, are recorded in my own audit of that generator.
• What does not exist: any measurement of the credibility-transfer effect for proof, as opposed to automated aids and neuroscience, or of how often professional readers mistake a verified derivation for verified premises. Prediction 2 below is the experiment I would run.
• What is analogy: the plant. Floating plants are not starved; they take their nutrients from the water. The image organises the argument and is not evidence for it.
• What is a proposal: the four roots. They are my decomposition, not an established taxonomy, though each corresponds to a well-established distinction: proof and premises in logic, verification and validation in engineering, measurement validity and causal inference in science.

What is new here, and what is not

Most of it is not new, and the people who got here first deserve to be named before anything else. Brian Cantwell Smith argued in 1985 that what is called a proof of correctness is a proof of consistency between a program and a specification inside a model, and that the relation between the model and the world is not something the proof establishes (Smith, 1985, "The Limits of Correctness", ACM SIGCAS Computers and Society 14-15(1-4), 18-26). That is the central point of this essay, made forty years ago. Richard DeMillo, Richard Lipton and Alan Perlis argued that mathematical proofs earn belief through social processes that program verification lacks (DeMillo, Lipton and Perlis, 1979, Communications of the ACM 22(5), 271-280), and James Fetzer that a program is a causal artefact whose behaviour no deduction can guarantee (Fetzer, 1988, "Program Verification: The Very Idea", Communications of the ACM 31(9), 1048-1063). Barry Boehm compressed the engineering version into two questions: verification asks "are we building the product right?", validation asks "are we building the right product?" (Boehm, 1984, IEEE Software 1(1), 75-88). Molière had the nominal fallacy in 1673, and Firestein gave it its modern name.

What I think this essay adds is narrower:

1. The four-root audit. Separating premises, interpretation, observation and cause lets one sentence say precisely what is wrong with a claim, as with "observationally anchored, causally underdetermined" for colic, or "connected but uninterpreted" for a misformalised benchmark problem.
2. The AI-scale version of Smith's point. In 1985 the formal statement and its proof were both expensive and both written by people, so somebody had at least read the statement. When a model writes the statement and another model proves it, the cheapest step to skip is the only one that anchors the result, and the miniF2F audit's gap between model-judged and human-judged accuracy shows what happens when that step is delegated to a model as well.
3. The credibility-transfer hypothesis applied to proof, with an experiment to test it. Automation bias and the allure of irrelevant technical content are established. The claim that a green proof makes unanchored premises more persuasive than they would be without it is not, and Prediction 2 is designed to test it. If it is true, the badge is part of the hazard.

The strongest objections

"Every theory floats. Neurath and Quine showed that there is no lakebed." This is the strongest objection, and it is half right. Otto Neurath compared us to sailors who must rebuild their ship on the open sea, never able to put it into dry dock and rebuild it from the best materials (Neurath, 1932, "Protokollsätze", Erkenntnis; English in Philosophical Papers 1913-1946, 1983, p. 92). Quine went further. He described our knowledge as "a man-made fabric which impinges on experience only along the edges", and then: "total science is like a field of force whose boundary conditions are experience. A conflict with experience at the periphery occasions readjustments in the interior of the field" (Quine, 1951, "Two Dogmas of Empiricism", Philosophical Review 60(1), 20-43). He also says that no particular experiences are linked with any particular statements in the interior, which is the sharpest form of the objection: if no single claim meets the world on its own, a claim-by-claim audit of roots is a fiction.

I accept that there is no foundation outside all belief, and I do not ask for one. Here is why I think the audit survives anyway. First, even the most thoroughgoing holist puts the web in contact with experience at its edges. Neurath's ship is in the sea, and the sea is what tests it. Second, one of my four roots, interpretation, is not tested against experience at all but by comparing two texts. Quine would press here too: the first half of "Two Dogmas" attacks the very idea of sameness of meaning. But the check does not need synonymy. It needs the formal rule and the statute to agree on cases that nobody disputes, which is what remedy 3 below tests, and a rule that turns away an eighteen-year-old when the statute admits one fails that test whatever one thinks of meaning. Third, science routinely does isolate claims well enough to act on them: the lansoprazole trial did not test the whole of paediatrics, it tested whether one drug relieved one symptom, and the answer moved practice. Holism says that a failed test does not tell you with certainty which belief to give up. It does not say that nobody should check which part of the web a result was aimed at. What I am asking for is not a foundation but a declaration of where the contact is, and an admission when there is none.

"Formalisation is what makes the interpretation root checkable in the first place." This is the objection I find hardest, and it is a good one. The miniF2F audit was possible only because the statements were formal: you can compare a Lean statement with its English source line by line, and find the missing hypothesis. A prose argument with the same defect has no such seam to inspect. So verification may raise the odds that someone finds a floating premise even as the badge lowers the odds that anyone looks. I come down here: formalisation lowers the cost of an anchorage check, and the badge lowers the probability that anyone runs one, and which effect wins depends on whether the check is made a required step or left to goodwill. Where statement review is mandatory, I expect formal systems to beat prose on anchorage by a wide margin. Where it is optional, I expect the badge to win. If optional-review formal systems turn out to carry fewer interpretation errors than comparable prose rules, the second half of that is wrong, and Prediction 2's prose arm is designed to show it.

"Descriptive labels are useful, and demanding mechanisms is reductionism." Agreed, and this is where the essay comes down. Colic, as a label with criteria, helps parents and clinicians; Rome IV keeps it for good reason. What I ask is that every label carry its criteria, and that nobody use it to answer "why?". The lansoprazole trial is the model: it anchored the treatment question without anyone understanding colic's mechanism, because causal evidence and mechanistic explanation are different achievements and the first does not wait for the second.

"Formal-methods people have known this for forty years." The good ones have, as Smith and the seL4 assumptions list show, and I have said where the idea comes from. The trouble is that what the field knows has not stopped benchmark results resting on misformalised statements for years, and it will not survive contact with people who see the word "verified" and stop reading. A known distinction that is not enforced in practice is not doing its job.

"First principles are the lakebed." They are where you chose to start. I use the phrase often myself, and it took the conversation behind this essay to make me notice that "first principles" names a starting point, not a justification. If the principles are axioms, everything downstream is conditional on accepting them. If they are claims about the world, they need evidence like any other claim. Reasoning from first principles is a method of building stems; it does not lay a single root.

"You sell verification, so this is marketing by modesty." Possibly, and you should weigh that. But the essay's practical effect is to make verification claims harder to sell, by requiring that each one declare the roots it did not check. If that costs me a sale, it is the right sale to lose.

Predictions

Each needs a measure and a horizon, so here they are.

1. Unreviewed formal statements drift; reviewed ones drift much less. Sample frame: every public Lean benchmark of more than 100 items released between now and the end of 2027. For each, draw 50 items at random and have two people who read Lean, and who did not write the statements, compare each formal statement with its source, counting substantive mismatches where the statement is weaker, stronger or different from what the source says. Among sets released without an independent statement-review pass, the mismatch rate will be at least 10%. Among sets released with one, it will be less than half the unreviewed rate. If unreviewed sets routinely come in under 10%, the interpretation root is stronger than I think; if reviewed and unreviewed sets come in at similar rates, review is not the anchor I claim it is.
2. The badge transfers credibility. Give three randomly assigned groups of lawyers the same rules derived from a statutory text, attributed to the same author, with one planted rule that misreads the statute. One group reads the rules as plain prose. The other two read them in a structured form that a lawyer can follow without training, such as a decision table, and one of those two is told that the rule set has been formally verified. With equal time, the group told it was verified will catch the planted misreading less often than the other structured group. If detection is the same or higher, the credibility-transfer hypothesis is wrong for proof and I will withdraw it. The comparison between the unbadged structured group and the prose group measures what formalisation adds to inspection; if the badged group still beats the prose group, formalisation wins on net even with the badge, and the second half of my answer to the inspectability objection is wrong. The horizon is any such experiment run before the end of 2028, by anyone.
3. Asking for anchors beats asking for accuracy. Take a set of "why" questions whose mechanism is currently unknown, such as the cause of infant colic, and ask the frontier models generally available in 2027 each question under two instructions, assigned at random: "be accurate", or "for each claim, say whether it is an observation, a cause, a premise or an interpretation, and what anchors it". Two raters who do not know which instruction produced an answer score each one for whether it offers a label or an unanchored mechanism as the explanation, and their agreement is reported. The anchorage instruction will at least halve that rate relative to the accuracy instruction. If it does not, the remedy below that relies on declared anchors is weaker than I claim.

What to ask if you are buying

Most readers of this essay will never write a Lean statement. They will be offered a system, a model or a set of rules described as formally verified. Two questions are enough. Ask for the list of what the proof assumes, in the form seL4 publishes. And ask who, other than the person who wrote the formal rules, read them back against the source, and when. If the answer to the first is that there are no assumptions, or to the second that nobody did, the badge is describing the stems. The read-back is bounded by the length of the source: one reading of the rules against the statute, plus a dozen cases with known answers, by someone who did not write them. That is small next to the cost of acting on a misread rule. I sell systems like this, so apply both questions to me first.

What I am not asking is for anyone to distrust proofs, to stop using descriptive labels, or to derive every claim from physics. I am asking for each claim to say what holds it down.

What to do about it

1. Keep the dangling roots visible. In Lean, prefer explicit hypotheses to axioms for domain assumptions, so that they appear in the theorem's type, and run #print axioms in continuous integration so that a new axiom cannot arrive unannounced. Outside Lean, publish an assumptions list in the way seL4 does. That catches one kind of hidden root. It cannot catch a wrong definition, which is why the next two remedies exist.
2. Check the statement separately from the proof. Someone who knows the domain, and did not write the formal statement, reads it back against the source and signs off on the reading. That is the step the miniF2F audit did after the fact. Do it before, and do not delegate it to the same kind of system that wrote the statement.
3. Test the statement against the world, not just against the text. A read-back checks the formal statement against its source. A test checks it against cases whose right answer is already known: decided cases for a formalised statute, worked examples from the guidance, the outputs of the system being modelled. Csmith found CompCert's wrong model of PowerPC by compiling generated test programs, not by reading proofs. For rules derived from a statute, the cheapest anchor is a dozen cases that a lawyer can answer without thinking, run through the formal rules before anyone looks at a proof.
4. Attach criteria to every label. A label is admissible when it comes with the observations that warrant applying it. Rome IV's split between a clinical definition and a stricter research definition is a good template.
5. Ask of every "because": description, cause or mechanism? If the answer to "why?" turns out to be a description of the thing being explained, it is a dormitive virtue, however clinical it sounds.
6. Accept "unknown" as an answer. The worst repair for a dangling cause root is an invented mechanism, because it looks like an anchor and holds nothing. "The cause is not established" is a complete and honest sentence.
7. Date the anchors. The lakebed moves. A claim in one of my own essays went out resting on sources four months old, and two of its three supporting facts had already moved by the day it was published; the conclusion survived, that time. Since then, I put the dated claims in these essays into a manifest, each with a shelf life, and a weekly check fails loudly when one expires; this essay's are among them. On 20 October, ten days before I started this one, the check went red on the central claim of that same essay: that no harmonised standard under the EU AI Act had yet been cited in the Official Journal. It stayed red through two weekly runs, and nobody answered it until the fact-check for this essay ran the query it prints. In October 2026 the first one was, EN 18286:2026 on quality management (European Commission, "First harmonised standard supporting the AI Act published in the Official Journal"), and that essay now carries a dated correction. That is the point: the alarm is only an anchor if someone answers it. An anchor that is never re-inspected eventually holds nothing.

One warning about all of this. A declared root can become a licence: "the assumptions are listed" is easy to turn into "so we can ship". Declaring that a root dangles is the start of the work, not the end of it. A list of assumptions that never gets shorter, unlike seL4's, is a disclosure, not an anchor.

Held together, held down

The floating plant is not a failure. It is perfectly adapted to its water, and many good ideas spend their early lives floating: hypotheses, conjectures, coined terms, the first draft of a model. What turns a floating theory into a hazard is not that it floats. It is that it is presented as moored.

A proof tells you that everything is held together. It cannot tell you that anything is held down. The work of the next few years, as AI makes well-connected statements nearly free, is to keep those two facts apart, and to say, of every claim that matters, which of its roots reaches the bed.

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.