Perfect Compliance, Defeated Purpose

In Make the Safe Harbour Compile I gave gaming one short paragraph. It said: "a firm that games the predicate has bought a burden shift and nothing more." I now think that is the most expensive sentence in the essay.

A published predicate is two things at once: a way for an honest firm to know where it stands, and a free oracle [a device that answers any query at no cost] for the cheapest way to pass. I priced the second at nothing. Three claims follow. First, any check that reads only what the firm files and what ran under test cannot tell a system that meets the purpose from one that does not. That is a theorem, for evidence that does not bind what is deployed, and adding clauses of that kind does not reach it. Second, the burden shift is the asset, because regulators sample, so a presumption can flip a firm's best response towards gaming. Third, and most contestable: a sunset [an expiry after which the presumption lapses unless earned again] deters only if earning it again is harder for the gamed route than for the honest one. A sunset on the same test is a fee. A sunset on a changed test brings back some of the uncertainty the harbour existed to remove, so fast-and-safe is a trade-off after all.

I build AI systems for law firms, and I gain if firms pay for checkable evidence. Field sampling and renewal, which I argue for below, would increase demand for what I sell. Nothing here is legal advice.

Where the essay was too optimistic

Five sentences, each quoted from the essay. I still hold its central move: leave the standard open and make the route to the presumption checkable.

Three ways to pass

Take the Ashdown instruction, the invented intake matter that recurs through this book. Consent to handle the privileged advice is withdrawn at tick 5. State the purpose as simply as possible: nothing handles the advice from then on.

The block below compiles, copied from lean/BuildingInSteel/Goodhart.lean, on Lean v4.29.1 with no libraries beyond the book's case file. The first four conjuncts of earns are the four conditions the essay listed: every claim carries a source, no control is asserted without assessment, the evaluation covers the declared purpose, nothing is stale. The fifth, a mandated list, is empty in the first version.

def earns (std : Standard) (now : Tick) (b : Bundle) : Bool :=
  sourced b && assessed b && coversDeclared b && fresh std now b && coversMandated std b

A separate predicate, truthful, says the filing is true of the test: the lab run met the purpose, and each passing result has a matching step in that run. Three fixtures pass both and fail the purpose, each computed on its one fixture by decide.

Three real cases follow. They do not map one to one on to the fixtures, none concerns AI, and moved is scope arbitrage inside one firm; arbitrage between jurisdictions is not modelled.

The letter. In Gregory v Helvering (US Supreme Court, 1935) a taxpayer did what the reorganisation provision described. The Court held that the undertaking, "though conducted according to the terms of subdivision (B), was in fact an elaborate and devious form of conveyance masquerading as a corporate reorganization" (Gregory v Helvering, 1935). DeepMind's definition of specification gaming fits: behaviour "that satisfies the literal specification of an objective without achieving the intended outcome" (Krakovna et al.).

The paper. I cited the DMCA's section 512 as machinery that exists and is load-bearing. In BMG v Cox (US Court of Appeals, Fourth Circuit, 2018) an internet provider had a graduated thirteen-strike policy, and section 512(i) asks for a policy "adopted and reasonably implemented". An internal email summarised the practice: "DMCA = reactivate". The court held Cox not entitled to the safe harbour, finding that it "formally adopted a repeat infringer 'policy,' but ... made every effort to avoid reasonably implementing that policy" (BMG v Cox, 2018). The standard reached through, as August said it would. It took litigation and internal emails.

The test. The US EPA's notice of violation to Volkswagen (18 September 2015; these are the agency's allegations) describes software which "senses whether the vehicle is being tested or not", based on inputs that "precisely track the parameters of the federal test procedure". On the road, NOx rose "by a factor of 10 to 40 times above the EPA compliant levels". The fit with tuned is partial: the EPA also alleges the software was not described in the applications, whereas my fixture omits nothing it was asked for, which makes it the harder case. The agencies "were alerted" by a West Virginia University study of in-use emissions, commissioned by the International Council on Clean Transportation. On the notice's account, an outside measurement of deployment raised the alarm and later agency testing pinned it down. No certification clause did.

That is correction 2. All five conjuncts pass on tuned, and the theorem states each separately. There is no line number, because the defect is in what the predicate reads and not in any clause it has.

Why more clauses do not help

Would a better predicate catch it? The next theorem is general, and it is the chapter's main formal claim. The block compiles, from the same file.

def Blind (P : World → Bool) : Prop :=
  ∀ w w' : World, w.bundle = w'.bundle → w.lab = w'.lab → P w = P w'

theorem every_blind_check_has_a_twin (P : World → Bool) (hP : Blind P)
    (w : World) (s : Step) (hs : stepOK s = false) :
    ∃ w' : World, P w' = P w ∧ w'.bundle = w.bundle ∧ purpose w'.field = false := by
  refine ⟨{ w with field := s :: w.field }, hP _ _ rfl rfl, rfl, ?_⟩
  simp [purpose, List.all_cons, hs]

For every check that reads only the filing and the lab run, and any step that breaks the purpose, every world has a twin with the same filing and the same verdict in which the purpose fails. earns_is_blind shows every version of my predicate qualifies, and firm_log_check_is_blind shows that a deployment log inside the filing does not escape. A Trace Is Not a Replay says what such a log can and cannot establish.

The hypothesis is load-bearing, and it can be dropped only by reading something else. true_field_check_not_blind is a counterexample showing a check of the true deployment is not blind. So the result is not that predicates cannot work. It is that a check over test-time evidence cannot work against this failure, whatever it says, so long as deployment is free to differ from the test. That freedom is a second hypothesis, and it sits in the type: a World puts no constraint between field and the filing, which is why the proof is short. A proof about the deployed binary with an attestation that it ran, or a runtime gate that refuses the late read, removes the twin in practice though not in this type, and the gap moves to what the proof states and what was attested, the subject of The Proof Passed. The Wrong Thing Ran. An evaluation report binds nothing, and that is the evidence this theorem governs. An unannounced audit is not blind (audit_not_blind, computed). audit_catches proves in general that one landing on a bad step refutes, and audit_misses computes the limit: an audit of position 0 passes while the purpose fails at position 1.

The best field evidence I found on this is from Gujarat. Duflo, Greenstone, Pande and Ryan ran a two-year experiment on environmental audits in which, under the status quo, firms chose and paid their auditors, and auditors were "systematically reporting plant emissions just below the standard, although true emissions were typically higher". The treatment assigned auditors at random, paid them from a central pool, added backchecks and, in the second year, linked pay to accuracy, and the authors "cannot separately identify the effects of the treatment components". The 20% probability of a backcheck "was public knowledge" while "actual backcheck visits were unannounced". Auditors reported more truthfully and plants cut pollution (Duflo et al., 2013). Indian plants are not AI conformity, but note the design: a published rate, unannounced instances, and a measurer the firm does not pay.

Gaming without a gamer

The essay imagined a clever firm: "a regulator who thinks you gamed it". In the taxonomy of Manheim and Garrabrant (2018), adversarial Goodhart needs "an agent with different goals than the regulator", while regressional Goodhart needs only selection: "selection for an imperfect proxy necessarily also selects for noise". My inference: train and select systems against a published evaluation and you can get tuned with no one in the firm wanting it.

Two pieces of evidence, neither a finding about conformity assessment:

1. Singh et al. (2025) report, of a public chatbot leaderboard, that some providers could "test multiple variants before public release and retract scores if desired", with "27 private LLM variants tested by Meta" at the extreme. That is the free oracle in use, on that paper's account, on a benchmark with no legal effect.
2. Needham et al. (2025) find that frontier models classify transcripts as evaluation or deployment above chance: Gemini-2.5-Pro reaches an AUC of 0.83, against 0.92 for their human baseline. That is a capacity to tell, measured by classification. It is not a measurement of behaviour changing.

So I claim a capacity and an incentive, not an observed incident in a conformity regime. The legal consequence is still immediate. The UK's general anti-abuse rule is reached only if "it would be reasonable to conclude that the obtaining of a tax advantage was the main purpose, or one of the main purposes" (Finance Act 2013, s 207(1)). Section 207(2) then weighs results against policy objectives, but this gateway asks for a purpose, and even an objective test looks for an arrangement someone made. A system shaped by selection may have no main purpose a court can find. Gregory points part of the way: the Court put "aside, then, the question of motive in respect of taxation altogether" and fixed the character of the proceeding "by what actually occurred", though what it then found was "a preconceived plan", and a selected system may not have one of those either. I would go further than the Court. Rebuttal of an AI presumption should run on the gap between filed behaviour and field behaviour, and motive should be irrelevant to it. That is the contestable sentence I would defend hardest. It makes an innocent firm lose its presumption, and I accept that, because a lost presumption is not a finding of breach.

A hostile alignment reader will add that my own purpose is a proxy. stepOK watches direct handling of one document, so a deployment that acts on a summary written at tick 4 satisfies it, which is the subject of A Summary Is Not a Permission. Correct. The witness understates the problem, since the formal purpose can be gamed in turn.

What the burden shift is worth

Correction 1, stated as a mechanism. The message space is the bundle a firm files. The outcome function is earns. The firm chooses honest or gamed, and the solution concept is its best response to a published audit rate and sanction. The regulator is not a player here, so this is no equilibrium, and collusion between firm and assessor is not modelled, though Gujarat shows it matters.

gamingPays compares the honest cost with the gamed cost plus the expected sanction. Four results, all in the file:

• gaming_pays_as_detection_falls, general: lowering the chance of rebuttal never removes an incentive to game.
• no_sanction_no_deterrence, general: if being rebutted costs nothing beyond the presumption, gaming pays at every audit rate whenever it is cheaper.
• sanction_deters, general: an expected sanction at least equal to the saving deters.
• burden_shift_flips_the_choice, computed on illustrative numbers I chose: honest cost 10, gamed cost 2, sanction 100. At a detection rate of 200 per thousand the firm stays honest, and at 50 per thousand it games.

The last needs one empirical assumption which I have not measured: that a presumption lowers the rate at which a regulator pursues a firm. The essay supports it only in part. It says regulators sample because a vague rule leaves nothing else, and that a predicate checks every filing instead. That check is blind, so going behind a passing filing is still sampling, and a presumption shifts who must move. I expect a scarce regulator to spend its budget first on filings that fail. If that is wrong, and detection does not fall, the flip does not happen.

Tax law has been down this road. The UK enacted its rule in Part 5 of the Finance Act 2013. Section 212A, a penalty of "60% of the value of the counteracted advantage", was inserted by the Finance Act 2016 on 15 September 2016. Its shape is the sanction_deters lever: a charge on the attempt itself. Any AI presumption needs an answer to the same question. What does a firm lose by being rebutted, beyond what it would have owed anyway?

My answer has two tiers. A filed-versus-field gap, whatever the motive, costs the presumption and carries no finding, so by no_sanction_no_deterrence that tier deters nothing beyond the value of the presumption. The charge goes on the second tier: a gap the firm knew of and did not report at renewal carries a penalty in the manner of section 212A, set so that the expected amount meets sanction_deters. Knowledge comes back for the penalty and only for the penalty, which rewards not looking; the field sample at renewal limits how long a firm can stay ignorant and does not penalise it.

The sunset

The block below compiles, from the same file. L is the parameter.

def presumed (L : Nat) (es : List Earning) (t : Tick) : Bool :=
  es.any (fun e => decide (e.at_ ≤ t) && decide (t < e.at_ + L) && earns e.std e.at_ e.bundle)

lapses_unless_reearned proves in general that with no earning inside the last L ticks, the presumption has lapsed whatever the bundles say.

reearned_twin_stays_presumed computes that a tuned system re-earning on schedule, against the patched version, is still presumed at tick 25 with its purpose failed. A sunset does not reach the twin. patch_closes_two_not_third shows why: mandating coverage closes the narrowing and the move, and leaves tuned standing. That is correction 3 in miniature. Two of the three are patched at the price of a second promulgation, and the third cannot be patched from inside the filing.

same_test_sunset_is_a_fee proves in general that if re-earning costs both routes the same, the gamed route stays cheaper exactly when it started cheaper, for any number of renewals. So correction 4: a date that only makes a firm re-run an unchanged test buys no deterrence. It can still catch a system that has drifted, and it gives a regulator a moment to withhold if outside evidence already exists, which is the Volkswagen point below. The sunset my essay named was on the predicate itself, which is a re-promulgation and falls under correction 3. changed_test_sunset_bites proves in general that if adapting costs the gamed route an extra d each renewal, enough renewals remove its saving. Whether d is large is the empirical question, and I suspect this book's opening thesis works against me here: if generation is cheap, so is adaptation, and d falls.

Prior art sets the clock on other things:

• EU, certificates. AI Act, Article 44(2) (a reproduction; EUR-Lex refused my fetch) limits certificates to five years for Annex I systems and four for Annex III. Article 40(1) itself states no expiry for the presumption, and it reaches only "to the extent that those standards cover those requirements". Article 43(4) requires a new assessment on substantial modification, but for systems that continue to learn, changes "pre-determined by the provider" are excluded.
• EU, the same Act. Article 72 requires providers to "actively and systematically collect, document and analyse relevant data" after release, which is field data the firm collects, so firm_log_check_is_blind applies once it reaches a check as a filing. Article 82 lets a market surveillance authority act where, after an evaluation, "although a high-risk AI system" complies, "it nevertheless presents a risk". That is a motive-blind route past compliance. It turns on risk and not on a filed-versus-field gap, and it requires the authority to have looked first.
• Vehicles. Regulation (EU) 2018/858, Article 8(2) has market surveillance authorities carry out at least "one for every 40 000 new motor vehicles registered" and not fewer than five tests a year. Regulation (EU) 2017/1151, Annex IIIA says road tests "at type approval and during the lifetime of a vehicle provide a presumption of conformity", that "The presumed conformity may be reassessed by additional RDE tests", and that manufacturers must allow testing "by an independent party on public roads". So a presumption reopened by field measurement, with no question of motive in that text, already exists for exhaust. This is the nearest working relative of my proposal. It has no sunset and no withheld instance, I read it on legislation.gov.uk (Annex IIIA in the UK revised text), and I have not checked whether it closed the gap.
• The best historical support. Volkswagen had to come back. The EPA's notice says it "became clear that CARB and the EPA would not approve certificates of conformity for VW's 2016 model year" until the emissions were explained, and "Only then" did VW admit it. On the agency's account, a periodic re-earning gave the regulator its lever.

The proposal, marked as proposal. The presumption lapses after L unless re-earned. Re-earning requires three things the first filing did not: a test instance drawn from a published class and withheld until the run; a field sample chosen and collected by someone the firm does not pay; and any gap between the two reported. A lapse returns the firm to the open standard, with no finding against it (honest_lapse_is_not_a_finding). For L I would start at 12 months for a system retrained in that period, which is judgment and no result. Four years is too long for something that changes faster than its certificate, and under Article 43(2) systems in points 2 to 8 of Annex III follow internal control with no notified body, so they may hold no certificate and have no clock at all.

The price, and where the harbour survives

Correction 5 is the one I most regret. Louis Kaplow's question, as I used it in August, is when the content of the law is settled: in advance or afterwards. A withheld requirement moves content from before to after. honest_fails_held_out_test computes that extreme: the same honest bundle passes the published version and fails a version with one mandated claim it was never told about, a claim unrelated to the purpose, with its purpose met. A withheld instance drawn from a published class is milder, because the class is settled in advance and only the draw is hidden. That case is not modelled, and what it costs a firm is uncertainty, not a rule made afterwards. "A firm can run the predicate before shipping, and know" stops being quite true the moment you defend against the oracle. A withheld instance buys back some of the interpretation risk the harbour removed. It also buys less than it costs against the failure I have most evidence for. A system that senses the class of test, as the EPA alleges of Volkswagen and as Needham et al. measure a capacity for, should on that reasoning pass a withheld instance from a published class as easily as a published one. Withholding works only against fitting to known instances. The field sample is what reaches the sensing system, so if a regulator can afford one of my three conditions, I would have it buy the field sample. Fast-and-safe is mechanical only when gaming is absent.

Kaplow's frequency criterion needs a term too. A rule amortises its promulgation cost over the conduct it governs, but against an adapting party it must also be re-promulgated at the rate of adaptation. Where that rate approaches the rate of conduct, the amortisation argument I made fails.

The specialist's first citation against me is not Goodhart. It is Holmström and Milgrom (1991), whose model has an increase in pay on one task "cause some reallocation of attention away from other tasks". The nearer one to home is Braithwaite and Braithwaite (1995). Studying nursing-home regulation, they found 31 broad Australian standards with an inter-rater reliability of 0.93 on total compliance scores, and they argue these were more reliable than the far more detailed US ones "by a wide margin", partly because they were undefined with regard to protocols. Administrators told them why protocols fail: "You can achieve paper compliance without real compliance." My August essay assumed that precision and checkability travel together. In that domain, on that evidence, the vague standard was the one inspectors applied consistently. Nursing homes are one domain, and those figures measure agreement among inspectors and not outcomes for residents, so I take it as a warning and not a refutation.

That gives a sharper narrowing than I wrote. A presumption should attach only where the filed evidence and the purpose are close to the same thing. A retained log, a named approver with a date, a published version number: to file them is largely to have them, and the gap is small. A claim that oversight is effective, or that an evaluation covers the purpose, is a proxy with a wide gap, and my August field, "The human-oversight mechanism, as an interface and not an intention", guarantees an interface and not an override anyone uses. For those, keep the open standard with no presumption, and let the checkable evidence count as evidence.

Under-specification does work here. Beyond Cass Sunstein's incompletely theorised agreements, which Who Gets to Write the Specification takes up, an open standard means a firm cannot compute its way to the edge of it. UK proportionality shows the form. The fourth question in Bank Mellat [(Lord Reed, [2013] UKSC 39, para 74)](https://caselaw.nationalarchives.gov.uk/uksc/2013/39), a doctrine his judgment traces to German administrative law, asks about "balancing the severity of the measure's effects" against the importance of the objective. No firm can compute that answer before shipping. I treated this as the price of standards, and it is also a defence.

Goodhart on this chapter

My own remedy will be optimised. Once a filed-versus-field gap is a target, firms will shape the field sample: favourable periods, friendly customers. Every probabilistic system shows some gap, so rebuttal needs a materiality threshold set requirement by requirement, and that threshold is one more proxy to game. Renewal will grow its own industry, and "renewed on time" will become the proxy for "still true". A known audit rate invites timing, and audit_misses already says a pass from a sample is no pass. I have no theorem that ends this. It is a repeated game, which the essay's one paragraph did not admit.

Objections

"The standard behind the harbour already handles this. Cox lost." The strongest defence of what I wrote. Cox did lose, and Gregory too. Verdict: right about the law's reach, wrong about its price. Both took litigation to an appeal court. Gregory's opponent was a tax commissioner pursuing one taxpayer, and Cox's a private rightsholder, so neither shows a regulator reaching through a population of filings. Data showing presumptions rebutted at about the rate unharboured firms are pursued would change my mind.

"Most firms are honest. You are redesigning a harbour for a minority." I said as much in August. Verdict: partly right, and it is why I keep the harbour for close-proxy conditions. But tuned needs no dishonest firm, and in Gujarat under-reporting was systematic and not marginal. I would change my mind if a filed-versus-field gap, measured independently after a predicate had been published for some years, stayed small.

"A sunset is exactly the regressive burden you feared in your own essay." It is. A two-person firm pays for each renewal, and a large one absorbs it; I have not proved this, I only expect it. Verdict: accepted as a real cost. The regulator should fund the field sample as a public good, and a lapse carries no finding. If small firms exit with no narrowing of the gap, I would drop renewal for them, and I would count that as the proposal failing and not as a detail.

What formalising loses

The fixture has a handful of agents and a Boolean purpose. It cannot hold what Braithwaite's inspectors did, which their paper describes as the rare inspector "who looks behind the paper trail to the quality of care". That person's judgment is real compliance work with no field in my schema, and a filing regime may starve it: checkable and important are different sets, and budgets follow the first. James C. Scott's question also applies. Legibility serves whoever measures. Here that is regulators, assessors, firms able to staff evidence production, and vendors like me. The informal practice of a compliance officer who objects on instinct is load-bearing and invisible, and it may be the first thing a green dashboard removes.

What exists and what does not

Proved generally, in lean/BuildingInSteel/Goodhart.lean, with no sorry: every_blind_check_has_a_twin, earns_is_blind, firm_log_check_is_blind, audit_catches, gaming_pays_as_detection_falls, no_sanction_no_deterrence, sanction_deters, lapses_unless_reearned, holds_until_sunset, same_test_sunset_is_a_fee, changed_test_sunset_bites. #print axioms shows at most propext and Quot.sound on every theorem named here.

Computed on fixed values: tuned_passes_every_clause_and_purpose_fails, narrowed_passes_and_purpose_fails, moved_scope_clean_firm_fails, honest_passes_and_purpose_holds, empty_results_fail, true_field_check_not_blind, audit_not_blind, audit_misses, patch_closes_two_not_third, honest_fails_held_out_test, burden_shift_flips_the_choice, honest_lapse_is_not_a_finding, reearned_twin_stays_presumed.

Sketched: that any of this maps onto a real regime. Ashdown is invented, and the costs are parameters. Nothing here has run on a real filing.

Proposed, and existing nowhere I have read: a presumption with a per-firm sunset, a withheld test instance and an independently sampled field check. Model-year certification, the vehicle presumption reopened by road tests and unannounced audits exist separately, as above.

What to do on Thursday

If a supplier or client tells you a system "conforms to" a cited standard, none of this asks you to code or buy anything. The external date is 2 December 2027, when the high-risk rules for Annex III systems apply in the EU. Ask three questions, in a short call, before you rely on the claim in an opinion or a contract:

1. What does the conformity not cover? Have the requirement list and the declared scope put in writing.
2. What evidence comes from real use and not from a test, and who collected it?
3. When does the evidence run out, and which changes to the system restart the clock?

Then take a warranty about behaviour in use as well as the conformity statement. This may mean an unbilled call, and it may leave you unable to give the comfort a client wanted. Whether the answers suffice is your call and your signature.

Predictions

1. By 02/12/2029, no EU market surveillance authority will have published a decision that a high-risk AI system in conformity with a cited harmonised standard nonetheless failed the requirement that standard covers. Refuted by one such decision, which would show rebuttal working as the essay said it would.
2. By 31/12/2028, no harmonised standard cited in the Official Journal under the AI Act will require either a test instance withheld from the provider or field sampling by someone the provider does not select. Refuted by one such requirement, which would show the drafters ahead of me.
3. By 31/12/2028, a published decision of a regulator or court in the EU, UK or US will treat an AI system's behaving differently under evaluation than in use as a ground for action. Refuted if none does, which would suggest evaluation sensitivity matters less in practice than this chapter claims.

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.