Who Gets to Write the Specification?

Most of what I have written on this site argues for moving authority away from persuasive prose and towards artefacts that a machine can check. Requirements should be records rather than paragraphs. A change to a specification should fail a build when it contradicts a rule written years ago. A safe harbour in a regulation should be something you can compile against. I still think all of that is right. This essay is about what it leaves out.

When a specification becomes executable, the question of who writes it stops being clerical. A paragraph of policy is read by people, and people interpret, bend, escalate and occasionally refuse. An executable specification is not interpreted. It is run, the same way, on every case, at whatever volume the organisation can feed it. Whoever decides what it says has decided the outcome for every case it touches, in advance, and nobody downstream is positioned to soften it.

The argument of this essay is that correctness, validity and authority are different properties, and that formal verification delivers the first and, at best, the second. Correctness means the system does what its specification says. Validity means the specification conforms to the rules above it: the statute, the board's resolution, the regulator's rule. Verification can check that too, if the higher rule is formalised as well. Authority means the specification was written by someone entitled to impose it, through a process the people bound by it can recognise. No kernel can check that, because the rule at the top of any system is not valid by any further rule; it is simply what the people running the system accept. A machine-checked system can enforce a rule nobody with authority properly approved, flawlessly, and the better the verification, the more flawlessly it will do so. My most contestable claim follows: formalisation makes authority matter more, not less, because it removes the downstream discretion that used to absorb and correct bad rules, and so it moves all of the political weight of a rule to the moment of authorship. The practical consequence is that an executable specification needs explicit rules about who may recognise, change and override it, recorded and enforced inside the same system, even though their authority comes from outside it. The policy-as-code repositories I have seen do have rules of change, but they are keyed to files and owned by engineers, a code-owners entry, rather than keyed to outcomes and owned by whoever owns the policy.

I build verified AI systems for law firms. That is a reason to read this essay as a limit on my own sales pitch, which is how I mean it.

The specification is not a transcription

It is tempting to think of a specification as a faithful copy of what the organisation already intends, written in a stricter language. It almost never is. Writing one forces decisions that the prose version left open, and each decision chooses between interests. In particular a specification decides:

1. which interests become constraints, and which are merely hoped for;
2. which exceptions are recognised, and which cases fall through to the default;
3. which costs enter the objective, and which are left outside it;
4. who may override an outcome, and with what record;
5. which disagreements are settled, and by whom.

Prose can leave all five open, and this is often its purpose. Cass Sunstein called the result an incompletely theorised agreement: people who disagree about principles can still agree on a rule, or on an outcome, and get on with things (Sunstein, 1995, "Incompletely Theorized Agreements", Harvard Law Review 108(7), 1733). I made a related argument in Make the Safe Harbour Compile: the vagueness of a legal standard is often a designed capability, not a defect. An executable specification can still be incompletely theorised: the code need not say why a write-off over £5,000 goes to finance, and three teams can sign the same table of outcomes for three different reasons. What it cannot be is an agreement on an abstraction that leaves the cases open. It has to return an answer on every case it decides, so someone has to choose one.

A rule that three teams agree on until you write it down

Take a rule from inside a law firm, simplified, and invented for illustration: fee write-offs need appropriate approval. Everybody agrees with it. Now ask three teams to make it executable.

Finance wants to protect realisation, the share of recorded time that is actually billed and paid, so anything over £5,000 goes to finance. The client team wants the relationship partner to decide write-offs of up to £20,000 for key clients, because a write-off is often part of keeping the client. Risk wants any write-off on a matter where the client has complained to come to risk whatever its size, because a write-off can be used to settle a complaint quietly, and complaints have to be handled properly.

Each of those is reasonable. Each encodes a different interest. Here they are in Lean, as one file that compiles on Lean 4.29.1 with no libraries.

structure WriteOff where
  amount    : Nat   -- thousands of pounds
  keyClient : Bool
  complaint : Bool  -- the client has complained about this matter
  deriving DecidableEq, Repr

inductive Approver | partner | finance | risk
  deriving DecidableEq, Repr

-- Finance: protect realisation. Anything over 5k goes to finance.
def financeRule (w : WriteOff) : Approver :=
  if w.amount > 5 then .finance else .partner

-- Client team: the relationship partner decides up to 20k for key clients.
def clientRule (w : WriteOff) : Approver :=
  if w.keyClient && w.amount ≤ 20 then .partner
  else if w.amount > 5 then .finance else .partner

-- Risk: a write-off on a matter with a complaint goes to risk, whatever its size.
def riskRule (w : WriteOff) : Approver :=
  if w.complaint then .risk else financeRule w

-- Where all three agree: small write-offs with no complaint.
theorem agree_small : ∀ a, a < 6 → ∀ k : Bool,
    financeRule ⟨a, k, false⟩ = clientRule ⟨a, k, false⟩ ∧
    financeRule ⟨a, k, false⟩ = riskRule ⟨a, k, false⟩ := by decide

-- Where they do not: a 10k write-off for a key client who has complained.
theorem disagree : financeRule ⟨10, true, true⟩ = .finance ∧
                   clientRule  ⟨10, true, true⟩ = .partner ∧
                   riskRule    ⟨10, true, true⟩ = .risk := by decide

-- Every disputed case on a grid of amounts, listed by the machine.
def grid : List WriteOff :=
  [1, 6, 10, 20, 25].flatMap fun a =>
    [true, false].flatMap fun k => [true, false].map fun c => ⟨a, k, c⟩

def disputed : List WriteOff :=
  grid.filter fun w => !(financeRule w == clientRule w && clientRule w == riskRule w)

#eval disputed.length   -- 13 of the 20 cases on the grid

-- The whole disagreement region, for every amount, not a grid.
theorem disputed_iff (w : WriteOff) :
    ¬(financeRule w = clientRule w ∧ clientRule w = riskRule w) ↔
    (w.complaint = true ∨ (w.keyClient = true ∧ 5 < w.amount ∧ w.amount ≤ 20)) := by
  obtain ⟨a, k, c⟩ := w
  by_cases h1 : 5 < a <;> by_cases h2 : a ≤ 20 <;>
    cases k <;> cases c <;> simp [financeRule, clientRule, riskRule, h1, h2] <;> omega

-- A rewrite of the client team's rule that changes no outcome, for every write-off.
def clientRule' (w : WriteOff) : Approver :=
  if w.amount ≤ 5 then .partner
  else if w.keyClient && w.amount ≤ 20 then .partner else .finance

theorem clientRule'_same (w : WriteOff) : clientRule' w = clientRule w := by
  obtain ⟨a, k, c⟩ := w
  by_cases h1 : 5 < a <;> by_cases h2 : a ≤ 20 <;>
    cases k <;> simp [clientRule, clientRule', h1, h2] <;> omega

The first two theorems are proved by decide, which means the kernel checked them by exhaustive evaluation. The first is a statement about every write-off of up to £5,000, in whole thousands, with no complaint; the second is about one case. The #eval counts the disputed cases on a twenty-point grid: thirteen. disputed_iff and clientRule'_same are proved by case analysis and omega, the decision procedure for linear arithmetic, using no axioms beyond propext, and they hold for every write-off, not just those on the grid. Nothing here is a claim about any real firm's policy. One detail is worth noticing before going on: risk's draft falls back to finance's rule whenever there is no complaint, so it has already sided with finance on every case without a complaint, including every one where finance and the client team disagree, without anyone asking it to. Whoever drafts the default takes a side.

Three things follow.

Each rule is internally impeccable. None of them is inconsistent, none fails to return an answer, and any one of them could be implemented and verified. A kernel would accept each of them, because there is nothing for it to check a rule against except the rule, or another rule someone has chosen to put above it.

The kernel can state exactly where they disagree. The grid is for reading; the theorem is the claim. disputed_iff says the three rules disagree on a write-off if and only if there is a complaint, or the client is a key client and the amount is over £5,000 and no more than £20,000. That is a statement about every possible write-off, and the kernel has checked it. A grid chosen by someone who did not know where the thresholds were could have missed the key-client dispute entirely; the theorem cannot. Three teams arguing in prose about "appropriate approval" are arguing about adjectives. Three teams looking at that region, and at the thirteen grid cases in three of which every team gives a different answer, are arguing about cases. Ten of the thirteen are two-way disagreements: seven turn only on whether there is a complaint, and there risk stands alone; three turn only on the key-client limit, and there the client team does. The three three-way cases are the real disagreement, now isolated. I made the general point in When the Spec Can Contradict Itself: the kernel is an examiner that cannot be flattered.

The kernel cannot say which rule is right. It cannot be flattered, but it can be instructed. Whichever rule is deployed, the kernel will enforce it faithfully, and it has no view about whether finance, the client team or risk had the standing to decide the key-client complaint case. That is not a gap that better tooling will close. It is a question about authority, and the answer has to come from outside the specification.

Correct, and without authority

The cleanest real case I know of is Australian.

Between 2015 and 2019 the Commonwealth ran an automated debt-recovery programme that became known as Robodebt. Its central rule took a welfare recipient's annual income, as reported to the Australian Taxation Office, and compared it with the fortnightly income the person had reported to Centrelink. Recipients were invited to confirm or correct the matched figures; where they did not, the annual income was spread evenly across the fortnights of the year, and where the averaged figure was higher, a debt was raised, leaving the recipient to prove otherwise. Entitlement under the social security law depended on what a person actually earned in each fortnight, not on an annual average, and a casual or seasonal worker could be assigned income for fortnights in which they had earned nothing. On 19 November 2019 the government announced that it would no longer raise debts on averaged income alone, and on 27 November the Federal Court made consent orders in Amato v Commonwealth declaring that her debt, raised that way, was not validly made. The Royal Commission that reported in July 2023 found that "Robodebt was a crude and cruel mechanism, neither fair nor legal, and it made many people feel like criminals" (Royal Commission into the Robodebt Scheme, 2023, Final Report, vol. 1, p. xxix).

The detail that matters for this essay is not that the system had a bug. As far as the public record shows, it did what it was designed to do. The averaging rule was the specification. And the people with authority were told. In 2014 the Department of Social Services' lawyers advised on the proposal from the Department of Human Services, which ran the scheme; a former DSS director described the advice as saying "the proposal needed to change substantially in order to proceed" (SBS News / AAP, 3 November 2022). In February 2015 the Executive Minute put to ministers recorded that DSS had advised that "legislative change would be ... needed", and the minister signed it. Eleven days later, the proposal that went to Cabinet avoided the point "by the simple expedient of not mentioning averaging and saying instead, falsely, that the new approach would not change how income was assessed or payments calculated" (Final Report, vol. 1, p. xxv). From 2016 members of the Administrative Appeals Tribunal set aside debts on the ground that averaging could not prove income. The department fixed each case and ignored the reasoning, and "the fact that Tier 1 AAT decisions were not published made it easier for it to do so" (p. xxviii).

A perfectly verified implementation of the averaging rule would have been exactly as unlawful as the real one. It might have been worse, because it would have carried a certificate. Read as a specification failure, the record is precise. A rule that changed the outcome for anyone whose income varied from fortnight to fortnight was presented to the people with authority as a change that altered none. The evidence that it was wrong was collected and then discounted by the department that would lose by acting on it: by November 2016 DHS's own lawyers were reporting on the tribunal decisions, and an internal analysis dismissed the criticism as "the comment of one lone tribunal member" (Final Report, vol. 1, p. 238). Both are failures of the secondary rules I come to below, and both are the kind a machine can make harder: an outcome diff that is computed and attached to the approval cannot be described away, and an appeal count that is published per clause is much harder to dismiss in a private memo. Robodebt failed on validity, against the Act, and on authority, in what Cabinet was told, and correctness is no defence against either.

Two other cases fail at the same point from different directions. In England in 2020, with exams cancelled, A-level grades were calculated by a standardisation model whose aim was "to ensure that the overall pattern of results for the 2019/20 cohort mirrored grade distributions of previous years to avoid grade inflation, and also to provide a means of standardising grades across centres" (Ofqual, 2021, "Grading gaps in summer 2020"), aims that followed a direction from the Secretary of State on 31 March 2020 (Ofqual, 2020, "Standardisation of grades in general qualifications in summer 2020: outliers"). For 39% of entries the calculated grade was lower than the grade the student's teachers had proposed. Four days after results day, on 17 August, Ofqual told the exam boards to award whichever was higher (Ofqual, 2021, "Grading gaps in summer 2020"). Here the authority was not in doubt: a minister directed it. Nor was the student-level diff hidden: Ofqual's own report on outlying students says its analyses "were considered prior to the release of A level results". What failed was what the rule made binding. The direction set the target as a national distribution, so a student whose calculated grade fell below the teachers' was a cost the rule had already accepted, not evidence against it, and the diff had no standing until results were published and people objected. In the Netherlands, the tax administration used (double) nationality as "an indicator in a system that automatically designated certain applications as risky" for childcare benefits, and in December 2021 the Dutch data protection authority fined it €2.75 million for discriminatory and unlawful processing (Racism and Technology Center, 24 December 2021, summarising the Autoriteit Persoonsgegevens decision); the government had already resigned over the wider scandal in January 2021 (BBC News, 15 January 2021).

Where discretion goes

Before rules were executable, much of their practical meaning was set by the people applying them. Michael Lipsky put it in one sentence in 1980: "the decisions of street-level bureaucrats, the routines they establish, and the devices they invent to cope with uncertainties and work pressures, effectively become the public policies they carry out" (Lipsky, 1980, Street-Level Bureaucracy, Russell Sage Foundation, preface; the sentence also appears in the preface to the 2010 expanded edition, linked). Mark Bovens and Stavros Zouridis described what happened when information systems took over that work: discretion did not disappear, it moved from the case worker to the system designer, the analyst and the person who writes the decision rules (Bovens and Zouridis, 2002, "From Street-Level to System-Level Bureaucracies", Public Administration Review 62(2), 174-184).

The question is who, in practice, ends up with it. The evidence suggests: whoever writes the code, by default. Danielle Keats Citron, citing the system's own decision-table release notes, reported that code writers had embedded more than nine hundred incorrect rules in Colorado's benefits management system between September 2004 and April 2007; a 2005 Deloitte review of the system, which she also cites, attributed incorrect rules in part to programmers' incorrect interpretation of policy (Citron, 2008, "Technological Due Process", Washington University Law Review 85(6), 1249). New Zealand's government, examining how legislation becomes software, observed that people had worked on drafting policy and on writing code from existing legislation separately, and called what lay between them "the translation gap between policy intent and implementation". Its response, a 2018 sprint called Better Rules, put policy developers, legislative drafters, service designers, rules analysts and software coders in one team from the start (OECD Observatory of Public Sector Innovation, "Better Rules for Better Outcomes"). Formalisation can also run the other way and expose the drift: when Denis Merigoux and colleagues wrote part of French family-benefits law in their language Catala, they found a bug in the official implementation (Merigoux, Chataing and Protzenko, 2021, "Catala: A Programming Language for the Law", Proceedings of the ACM on Programming Languages 5(ICFP), 1-29).

So the street-level case worker, whatever their faults, was a place where a bad rule could meet resistance. Lipsky's officials bent rules for sympathetic cases and enforced them harshly on others, and much of that discretion was arbitrary or worse. But it was also slack: a case worker who could see that a debt was absurd could refuse to raise it, or at least escalate. An executable specification removes the slack along with the arbitrariness. What remains is the rule, applied identically to everyone, and the authority of whoever wrote it.

This is why I say formalisation makes authority matter more. In a prose system, a rule nobody with authority properly approved is diluted by thousands of human readers, some of whom will decline to apply it. In an executable system, it is applied at full strength, every time, to everyone, and the only check left is the one at authorship. If that check is a code review by an engineer who was told to implement the policy, there is no check.

The same problem inside a firm

None of this is confined to governments. A firm that moves its policies into executable form, whether as policy-as-code, as an agent's instructions, or as a verified specification of the kind I advocate, recreates the same structure on a smaller scale.

In Refactor the Workflow, Not the Worker I argued that a workflow redesign is justified only relative to an observation, the list of events that the redesign must preserve, and that whoever writes the observation decides what the redesign may destroy. That is the same question in miniature. A redesign that keeps "an approval happened" but drops "by whom" is a correct implementation of a careless specification. In Nobody Is Paid to Delete I argued that a rule corpus written by authors with short tenure grows without bound, because nobody bears the cost of keeping a rule. Executable policy inherits that problem and adds a sharper one: every clause someone adds changes outcomes, immediately, everywhere.

And in Floating Theories I argued that a proof secures its conclusion relative to its statement, and that a green proof lends credibility to whatever the statement assumed. The authority behind a specification is one more premise of that kind. The kernel never sees it.

Hart's missing rules

Law has a well-worked answer to the question of what makes a rule binding, and it is directly usable. H. L. A. Hart argued that a system of rules that only told people what to do, which he called primary rules, would suffer from three defects: uncertainty about which rules are valid, a static character because there is no way to change them deliberately, and inefficiency because there is no authoritative way to settle disputes about them. Mature legal systems cure these with three kinds of secondary rules: a rule of recognition, which identifies the valid rules; rules of change, which say who may create, amend and repeal them; and rules of adjudication, which say who decides whether a rule has been broken (Hart, 1961, The Concept of Law, Clarendon Press, chapter 5).

Most executable specifications I have seen consist entirely of primary rules. They say what the system does. They are silent on which version is authoritative and who signed it, on who may change which clause and through what review, and on who decides when a case is contested. That silence does not mean nobody holds those powers. It means they are held by default, usually by whoever can merge to the main branch, or by whoever a code-owners file names for that path, which is a rule of change keyed to files rather than to outcomes.

Translated into a specification system, the three secondary rules look like this.

Who counts as a clause owner is not something the file can settle. The system can record and enforce the answer; the organisation has to supply it. And recognition that only the organisation can see is not recognition by the people bound by the rule, which is why the first row ends with them.

The second row is the one that does the most work, and it is mechanical. Where the inputs are structured, as they are here, the test needs no reference set at all: prove that the new rule gives the same answer as the old one for every input, as clientRule'_same does for a rewrite of the client team's rule, and the change is a refactoring by proof. Where no proof is available, run old and new over a reference set of cases. If any outcome changes, it is a policy change, and the diff of outcomes is what the policy owner should be shown, not the diff of code. If none changes, the change is a refactoring only on that set, so the set itself is where power now sits. It belongs to the clause owner, not to the engineer, and every upheld appeal and every override is added to it automatically. Until a change is proved or diffed, it is a policy change by default.

The fifth item in my opening list, which disagreements remain unresolved, also has a formal answer. Where the owners have genuinely not agreed, the honest specification does not pick a side silently. It leaves the point as a named parameter whose value is set, and recorded, by whoever has authority to set it. When I formalised Anthropic's published constitution for Claude, the most useful output was a list of the free variables it left open (Type-Checking the Constitution). A specification that declares its open questions does not pretend to an agreement it lacks. The owners agree on every case outside the parameter, each for their own reasons, and the cases inside it are settled by someone with authority, on the record. That is Sunstein's agreement on outcomes with its edge marked, which is the version that can survive being executed.

What exists and what does not

• What exists: the Lean file above, which compiles, and whose four theorems are proved about the three illustrative rules and one rewrite of them, and nothing else; the public record of Robodebt, the 2020 grading model and the Dutch benefits case, as cited; the literature on discretion moving into systems.
• What does not exist: any measurement of how often outcome-changing specification changes are approved by someone with policy authority. I do not know of one, and the first prediction below is that someone should make it. Nor do I know of a measurement, for proof, of the credibility transfer that the first item under "What is new here" relies on; Floating Theories states it as a hypothesis and sets out the experiment.
• What is a proposal: the mapping of Hart's secondary rules onto specification systems, and the outcome-diff rule for changes.
• What is invented: the write-off rules. They are an illustration, not any firm's policy.

What is new here, and what is not

The core observation is old. Lawrence Lessig argued in 1999 that in cyberspace code regulates behaviour as law does, and that whoever writes it is making policy (Lessig, 1999, Code and Other Laws of Cyberspace, Basic Books). Lipsky and then Bovens and Zouridis traced discretion from the street to the system. Citron argued that automated decisions need due process at the point where rules are coded. Deirdre Mulligan and Kenneth Bamberger argued that governance by design lets values be embedded in technology without the public deliberation that legitimates ordinary policy (Mulligan and Bamberger, 2018, "Saving Governance-by-Design", California Law Review 106(3), 697). Rónán Kennedy has examined rules as code against the rule of law and the need for judicial review of administration by software (Kennedy, 2024, "Rules as Code and the Rule of Law: Ensuring Effective Judicial Review of Administration by Software", Law, Innovation and Technology 16(1), 170-193). Brian Cantwell Smith argued in 1985 that a proof of correctness is only as good as the model it is stated against, a point I leaned on in Floating Theories. Hart's secondary rules have been applied to technical systems before: Marco Crepaldi used them to argue that public blockchains lack rules of recognition, change and adjudication (Crepaldi, 2019, "Why Blockchains Need the Law", ICAIL, 189-193).

What I think this essay adds is narrower.

1. The point is aimed at formal verification, not just at automation. The literature above mostly concerns opaque or buggy systems. The cases where the system faithfully executed a rule that should not have been the rule are the ones that formal methods do little to prevent unless the higher rule is formalised too, and, if the credibility transfer I argued for in Floating Theories holds for proof, they are the ones that verification makes more persuasive; that essay's second prediction is the test. Verification people have long said that a proof is only as good as its specification. We have mostly not said that writing the specification is an exercise of authority that needs its own rules.
2. The kernel's political use is converting agreement on words into agreement on cases. A proof assistant can state exactly the cases where candidate rules disagree. That turns an agreement on an abstraction, which hides disagreement until it is executed, into an agreement on particular outcomes, which Sunstein argued is the form of agreement that survives disagreement about principle.
3. The outcome-diff test makes the rule of change mechanical. Comparing outcomes before and after a change is old practice under the names characterisation testing and differential testing. What is new is routing approval on its result, by proof where the domain allows and by a reference set the policy owner controls where it does not.

The strongest objections

"Discretion was where the bias lived. Removing it is the point." This is the strongest objection, and it is substantially right. Lipsky's own account is full of rationing, favouritism and arbitrary harshness, and an executable rule is at least the same rule for everyone. Where I come down: removing discretion from the application of a rule is good, provided the discretion has somewhere legitimate to go. The Dutch case shows that a model can encode discrimination as reliably as a clerk can, so uniformity is not fairness. What the executable system needs is not case workers' discretion back, but a visible place where authority over the rule sits, an override channel whose decisions are recorded and audited, and a route by which overrides change the rule. If override channels in practice reintroduce the old arbitrariness at scale, I am wrong about the third row of the table.

"A uniform rule is also uniformly reversible. Robodebt was undone in bulk precisely because it was one rule." True, and it is the best thing to be said for executable policy: case workers err idiosyncratically, and their errors can never be reversed in one stroke. But Robodebt's reversal came years after tribunal decisions began setting its debts aside. Those decisions were unpublished, as Tier 1 decisions generally were, and the department that read them chose to ignore them. Uniformity makes a bad rule correctable in one stroke only if the evidence that it is bad accumulates somewhere the people with authority must look at it. That is what the appeal and dispensation records in the table are for, and why remedy 8 publishes them: a count read only by the operator is the record Robodebt already had. If organisations with executable policy and no such record turn out to correct bad rules as fast as those with one, I am wrong about the third row.

"Robodebt was a failure of law and politics, not of specification." It was a failure of law and politics, and it had secondary rules: Cabinet approval, a signed minute, a statutory duty to have regard to tribunal decisions. The people who held authority got round them. What survives that is the difference between a described change and a computed one. The failure sat where this essay locates it: the people who had authority over what the system ran were told the rule needed a change in the law, and the description of the rule they approved said otherwise. A computed outcome diff cannot say "this changes nothing" about a rule that changes the debt of everyone whose income varied, and an appeal count published per clause is much harder to dismiss in an internal analysis as the view of "one lone tribunal member". Officials willing to mislead Cabinet could also skip the diff or merge round a build rule, which is why prediction 1 measures bypasses and remedy 8 makes the counts public rather than leaving them to the operator.

"Requiring policy owners to approve changes will grind delivery to a halt." Changes that provably alter no outcome go through with an engineer's review. Changes that alter outcomes are policy changes, and routing them to someone with authority is not overhead; it is the only thing that makes the change legitimate. How many changes fall into each class is unmeasured. If most alter outcomes, then the policy owner's workload is the real cost of running policy as code, and it was being paid before, invisibly, by whoever merged.

"Legitimacy is for governance committees, not engineers." In principle, yes. In practice, the authority to change an executable specification sits with whoever can merge to it, unless something else is written down. Nobody chose Colorado's more than nine hundred incorrect rules. Some were mistakes and some were programmers' readings of policy, and because programmers altered rules, in Citron's words, "in ways the public, elected officials, and the courts cannot review", nobody with authority could tell which was which. Engineers do not need to decide what is legitimate. They need to build systems that refuse to run a policy change nobody with authority approved.

"Your earlier essays argued for exactly the concentration of power you now warn about." They argued for checkable artefacts, and I still hold that a checkable rule is better than an uncheckable one. This essay adds the condition I left implicit: a checkable rule needs checkable authority. Without it, verification is a way of making whoever holds the editor more powerful and more credible at once.

"You sell this." I sell verification. This essay is about a property that verification cannot supply, so its practical effect is to make what I sell harder to oversell.

Predictions

1. Outcome-changing changes mostly lack a policy owner's approval. In organisations that run policy as code, take a year of merged changes to the policy specification and replay each against a reference set of cases. Of the changes that alter at least one outcome, more than half will have been approved by engineering review alone, with no recorded approval from a named policy owner, wherever no build rule requires one. Where such a rule exists, the share of outcome-changing changes that bypassed it, through emergency merges, administrator overrides or changes classified as refactorings that the replay shows were not, will exceed 10%. This is testable within a year by any organisation with a policy repository and a reference set. If the first share is below a quarter, the default-authorship problem is smaller than I think.
2. Formalisation without an override channel raises the rate at which decisions are overturned. In public bodies that replace case-worker decisions with executable rules, the share of appealed decisions overturned on internal review or external appeal, reported alongside the appeal rate itself, will be higher in the two years after the change than in the two years before, unless the new system includes appeal and dispensation channels with recorded reasons. Where it does, the overturn share will not rise. If the appeal rate falls while the overturn share rises, the slack has moved to the few people able to appeal. The Royal Commission described that pattern in Robodebt without the numbers: seeking review required an understanding of the debt "which was virtually impossible to ascertain on the DHS documents", and a number of averaged debts that did reach the tribunal were set aside. If dispensations are available but used in fewer than 1% of cases, the channel has failed in the opposite direction from the one my first objection fears. I do not know of a public dataset that publishes both rates for an automated scheme, which is itself a finding; a body adopting rules as code could publish them from the start. If overturn shares fall regardless, the slack I am describing was not doing the work I claim.
3. Enumerated disagreement settles disputes faster than redlined prose. In disputes over the wording of an internal policy, randomly assign half to be negotiated on a redlined text and half on the machine-generated list of cases where the competing drafts disagree. The second group will reach a signed rule in less elapsed time, and will report fewer post-adoption disputes in the following six months. If there is no difference, the enumeration is a curiosity rather than a tool.

What to do about it

If you are a partner and not the person building any of this, the ask is smaller. Find one rule your firm already runs by machine (write-off approval in the billing system, conflict-check clearance, a client-onboarding threshold) and ask two questions of whoever configures it: who approved the last change to it, and were they shown which matters it would affect? If the answer to the first is the person who made the change, or the second is no, your firm has primary rules without secondary ones. I am not asking anyone to learn a proof assistant or buy a product. Steps 1 and 6 below are organisational, and so is the routing decision in step 3; enforcing it in the build, and steps 2, 4, 5, 7 and 8, need someone technical as well, and need not be you.

1. Name an owner for every clause of an executable policy, and record whose interest the clause protects.
2. Keep a reference set of cases for each policy, including the awkward ones, owned by the clause owner, and replay every change against it. Add every upheld appeal and every dispensation to it.
3. Route outcome-changing changes to the clause owner, with the diff of outcomes, not the diff of code. Enforce it in the build.
4. Formalise competing drafts before arguing about them, and argue about the list of disputed cases.
5. Leave genuine disagreements as named parameters, set and recorded by someone with authority, rather than letting the implementer choose a default.
6. Build the appeal and dispensation channels before go-live, each with a named decision-maker and a recorded reason for every decision, and review recurring ones monthly.
7. Make the outcome diff impossible to misdescribe. Robodebt's proposal told Cabinet that income assessment would not change. A computed diff of outcomes, attached to the approval, would have said the opposite on its first line.
8. Show the people bound by the rule which clause decided their case, and publish the count of upheld appeals and dispensations per clause. Robodebt's recipients could not easily tell from the letters what had been done to them, and the tribunal decisions that would have shown the pattern were unpublished.

Where the politics goes

The hope behind a lot of formal-methods writing, including mine, is that precision dissolves disagreement: write the rule exactly, check it mechanically, and the argument is over. Precision does dissolve one kind of disagreement, the kind where people thought they agreed and did not. It makes the other kind sharper. When the specification is executable, the politics does not disappear into the code. It moves to the moment of authorship, and it becomes operational there, on every case, at scale.

So the question to ask of any verified system is not only whether it does what its specification says. The kernel can answer that. The question is who wrote the specification, who was allowed to change it, and who could say no. The kernel cannot answer any of those, and the organisation must.

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.