A Proof Is Not an Appeal

In April 2021 the Court of Appeal described how the Post Office had prosecuted people on the strength of Horizon, its accounting system. "By representing Horizon as reliable, and refusing to countenance any suggestion to the contrary, POL effectively sought to reverse the burden of proof: it treated what was no more than a shortfall shown by an unreliable accounting system as an incontrovertible loss, and proceeded as if it were for the accused to prove that no such loss had occurred." The next sentence: "Denied any disclosure of material capable of undermining the prosecution case, defendants were inevitably unable to discharge that improper burden" [(Hamilton v Post Office [2021] EWCA Crim 577, [137])](https://caselaw.nationalarchives.gov.uk/ewca/crim/2021/577).

That paragraph is about who must prove what, and who holds the material. This chapter models both as a small game.

Thesis. The presumption that a computer worked should be earned, where software output decides an issue, by tendering an anchored record and a checkable certificate and handing both to the other side. That changes the game Horizon defendants were losing. It does not give anyone an appeal. A proof is relative to a specification, so a person harmed by the specification loses every contest about the run, however good the evidence. Whoever claims a presumption on the strength of proof must also offer a route to a forum that can hear the rule, name who adopted it, and reach every decision made under it.

Two findings would show me wrong. If disclosure rules alone, with no evidence tier, produce the same behaviour from parties relying on software, the tier is decoration. If disputes over automated decisions turn almost entirely on whether the system followed its rule, and hardly ever on whether the rule was lawful, the second half of the thesis is a philosopher's worry.

A disclosure. I build AI systems for law firms, and a rule that rewards checkable evidence would favour what I build. Discount the first half of the thesis accordingly. The second half argues against the sufficiency of my own product category.

What the law says, and what has happened since

This section concerns England and Wales. None of it is legal advice.

Until 2000, section 69 of the Police and Criminal Evidence Act 1984 made a statement in a computer-produced document inadmissible unless it was shown "that at all material times the computer was operating properly", or that any fault did not affect the document. The Law Commission recommended repeal in 1997, and section 60 of the Youth Justice and Criminal Evidence Act 1999 did it. The Ministry of Justice now describes what replaced it as "a common law (rebuttable) presumption that the computer was operating correctly at the material time" (MoJ, Call for Evidence, 2025). The wording in the Law Commission's report, which footnotes Phipson and which I have only as quoted by its critics, is "In the absence of evidence to the contrary, the courts will presume that mechanical instruments were in order at the material time" (Ladkin et al., 2020).

The reform has not arrived. In date order:

1. 21/01/2025 to 15/04/2025. The Ministry's call for evidence ran, on criminal proceedings only. It is closed. It promised that "A paper summarising the responses to this call for evidence will be published in due course". On 02/11/2026 the GOV.UK record still showed a closed call, no outcome, and one change-history entry, "First published."
2. 10/03/2026. At Lords Report on the Victims and Courts Bill, Amendment 21 proposed that "The common law presumption of the reliability of evidence referred to in subsection (1) is removed." The Minister, Baroness Levitt, said the call for evidence "demonstrated a lack of consensus as to whether there is even a problem", and offered, in place of its statutory scheme, rules of court for "cases where the introduction of computer-generated evidence could be determinative of an issue in the case". The amendment was withdrawn (Hansard, HL, 10/03/2026). The Act's table of contents has no computer-evidence entry.
3. 01/05/2026. The Criminal Procedure Rule Committee "discussed the potentially severe consequences of any requirement that the correct working of a computer must be established in every case in which computer output is in evidence", and approved proposed amendments "for consultation by ministers" with the peers concerned (minutes).
4. After that, I can find nothing. The word "computer" does not occur in the June or July minutes, or in the amendment rules mainly in force from 05/10/2026.

So on 02/11/2026 the presumption stands, and I could find no public rule text. Asked about civil proceedings, the Minister said they were "plainly not within the scope of the Bill".

A second presumption must not be confused with this one. On 08/10/2026 the Law Commission opened a consultation, closing 14/01/2027, on civil product liability under Part 1 of the Consumer Protection Act 1987. It proposes treating software and AI as products, and "a rebuttable presumption of defect" in cases of exceptional evidential difficulty, subject to strict thresholds, with a defendant who accepts it paying from a starting point of "50% of the damages" (Law Commission summary). That is a provisional proposal about compensation, and it runs against the defendant, a producer or other liable party. The criminal presumption is common law about evidence, and it runs for whoever relies on the machine. The EU reformed its directive in 2024; I could not download it. The Law Commission is also considering separate presumptions of fact, confined to particular factual issues, where "an asymmetry of information exists in the defendant's favour" and it would be fair for the defendant to carry the burden. There the burden follows access. The criminal presumption does not: it gives the first move to the opponent whether or not she has access, which is the complaint of this chapter.

What Horizon does and does not show

Three judgments carry the facts. In Bates (No 3), a civil judgment of 15/03/2019, Fraser J tried the contracts [([2019] EWHC 606 (QB))](https://caselaw.nationalarchives.gov.uk/ewhc/qb/2019/606). In Bates (No 6), of 16/12/2019, he tried the system: "In summary terms only, Legacy Horizon was not remotely robust" [([2019] EWHC 3408 (QB), [975])](https://www.judiciary.uk/wp-content/uploads/2019/12/bates-v-post-office-judgment.pdf). In Hamilton, a criminal appeal, the Court of Appeal allowed 39 appeals and dismissed 3. Parliament then legislated, "Every conviction to which this Act applies is quashed on the coming into force of this Act" (Post Office (Horizon System) Offences Act 2024, s.1(1)), a class that excludes convictions already considered by the Court of Appeal. The Ministry's final figures, correct to 15/09/2026, count 620 individuals with at least one conviction quashed by the Act (MoJ). The statutory Inquiry has published only a first report volume, on compensation and human impact, according to its news page, so I rely on the judgments, two of them after trial.

A tidy version of the story says the presumption caused the convictions. I do not think the judgments support it. In the copies I searched, the word "presumption" appears in neither Hamilton nor Bates (No 6); the only hit for the stem is "presumably". Bates (No 3) does use the word, in the Post Office's pleading quoted below, and I deal with it there. Hamilton's ground is "failures of investigation and disclosure". The Ministry's own press release carries the bullet "Presumption computer evidence is correct proved flawed during Horizon scandal", and then says the miscarriages "were down to deliberate failures to properly interrogate and disclose evidence" (MoJ, 21/01/2025). Against that, Marshall and colleagues write that "The central problem is the evidential presumption that computers are reliable" (Marshall et al., 2021).

I come down here: the judgments establish a mechanism and not a doctrinal cause. A party could assert reliability, hold the material, and leave the other side to prove a negative. The presumption is one route into that position. The contract was another. In the civil litigation the Post Office pleaded, as the judgment quotes at [673], that subpostmasters bore the legal burden on shortfalls because "the truth of the matter lies peculiarly within the knowledge of Subpostmasters", and that "it would not be right to infer or presume that a shortfall and loss was caused instead by a bug or error in Horizon". That is a pleaded presumption against a Horizon explanation, argued as an inference from branch management and not as the common-law rule about computers. Fraser J found the access ran the other way. Under one standard contract, "there is a contractual burden upon the Post Office to demonstrate that the loss for which it seeks to hold a SPM responsible was caused by the negligence, carelessness or error of the SPM", and subpostmasters "have no access to data between the Post Office and its clients" ([2019] EWHC 606 (QB), [654], [655]). Under the other, once the Post Office had shown a real loss, the burden of bringing it within the sole exception fell on the subpostmaster ([687]). On whether a subpostmaster must prove a Branch Trading Statement wrong, "imposing such a burden upon an SPM would be requiring them to perform the impossible" ([852]), "There was no mechanism adopted by the Post Office to resolve such disputes" ([1116]), and the answer to Common Issue 13 was "No, SPMs bear no such burden." ([1122]) The same answers held the wide no-fault liability term in one of the two standard contracts unreasonable under the Unfair Contract Terms Act 1977.

One trial was about the run: did the system do what it was said to do? Another was about the rule: what could the contract lawfully say? Horizon needed both.

The game

I use the Ashdown instruction, the book's worked example, an invented legal-intake case. Suppose the firm relies on its research agent's record to say the privileged advice never left. That dispute would be civil, so read what follows as structure and not as doctrine.

The model has a proponent, an opponent and three regimes. The presumption puts the opponent first, always. A rule with no presumption, the shape of section 69, puts the proponent first, always. The tier rule, my proposal, puts the opponent first only if the proponent has earned it: an anchored record, a passing check against the specification, and disclosure. This compiles on Lean v4.29.1 with no libraries, copied from lean/BuildingInSteel/Presumption.lean.

def burdenOn : Regime → Dispute → Party
  | .presumption, _   => .opponent
  | .tiered, d        => if earned d then .opponent else .proponent
  | .noPresumption, _ => .proponent

def finding (r : Regime) (d : Dispute) : Bool :=
  match burdenOn r d with
  | .opponent  => !rebutted d || d.tender.otherProof
  | .proponent => d.tender.otherProof

The opponent rebuts if a disclosed record fails the check, or if she holds independent evidence that the record is false or the run did not conform. That bar is higher than the law's. The Ministry says the burden shifts "if it can be shown that the software may not have been functioning correctly", and the Minister says a defendant need only raise "a real issue". So presumption_blind describes an opponent who can raise nothing at all, and the first column below overstates the presumption's grip on one who can raise a doubt. What the model keeps is the point at paragraph 137: without the material, even a doubt is hard to raise. otherProof stands for every other way of persuading a court. The model has no standard of proof, admissibility or sanctions, and its run field is what really happened, a view no court ever has.

regime_table proves all fifteen findings below for these five disputes, with no other proof tendered in any of them. "Yes" means the court finds the system worked. The last column is "no" by definition: that regime returns otherProof, which is false throughout, so even a perfect record counts for nothing in it. That is the model's way of saying the proponent must prove reliability by other means, and not a claim that a court would disbelieve such a record.

The presumption is blind without access. presumption_blind is general: for every dispute with no disclosure and no independent evidence, the finding holds, whatever happened. presumption_not_sound exhibits the failure on a faithful record. withholding_weakly_dominates is also general: any tender that wins disclosed wins withheld. withholding_strictly_better shows disclosure losing where withholding wins. The evidential game does not reward handing the material over. English law supplies that from outside the game, as a prosecutor's duty, and a breach the other side cannot see is what paragraph 137 describes.

The tier rule is sound on a faithful record. This is the main positive result. It compiles; the statement is copied from the file and its proof omitted here.

theorem tiered_sound (d : Dispute) (hf : d.tender.record = d.run)
    (hp : d.tender.otherProof = false) (hfind : finding .tiered d = true) :
    Conforms d.spec d.run = true

presumption_not_sound is the same two hypotheses with the opposite conclusion. The proof uses only the check on the record; anchoring and disclosure earn their place through the incentive and failure rules below, not through soundness. undisclosed_certificate_earns_nothing and damaging_record_cannot_buy_presumption are general: without disclosure, or with a record that fails the check, the burden stays with the proponent. tier_rule_rewards_disclosure shows the incentive reversed, on one honest certified case.

The hypothesis cannot be dropped. forged_record_earns_presumption is a clean, anchored, disclosed record of a run that did not happen, and it wins. own_evidence_rebuts_forgery shows that independent evidence defeats it, on that one forgery. The Ministry already said as much: "Any changes to the presumption would not be able to further protect against instances where parties mislead a court on the accuracy of the evidence." Anchoring attests the log and not the world, as A Trace Is Not a Replay proves in its own model. The tier rule also raises the return to a clean record, so rebuttal must stay.

Neither regime dominates. no_regime_dominates shows the presumption right and the tier rule wrong on an honest system with poor evidence, and the reverse on a withheld leak. That cost falls on whoever keeps poor records.

Proved: everything named, on these definitions, with #print axioms showing at most propext and Quot.sound. Sketched: that courts behave like this function. The certificate check here is a recomputation, so the model does not show the gap between finding a proof and checking one.

What the tier would require

Nothing in this section exists as law, and I have not built it. Scope. Evidence generated by software and determinative of an issue, borrowing the Ministry's boundary and the Minister's word. Everything else stays under the presumption. Tender. Four items, all required.

1. An anchored record: the harness signs, independent witnesses co-sign a published head, and writes fail closed. The evidence manifest in A Trace Is Not a Replay sets out the roles.
2. A certificate naming a stated specification and the SHA-256 digest of that head over one stated canonical serialisation, from a checker the generator cannot reach.
3. Stored model outputs and tool results, so the deterministic steps can be replayed. Regenerating the model's output is not required, for the reasons in the previous chapter.
4. Disclosure of the record, the specification and the known defects.

Failure. A missing artefact, a head older than a bound the rules of court would set, a witness disagreement or a compromised key drops the affected period to bare. The burden returns to the proponent, and no certificate rescues it. Who. In criminal cases I would apply the tier to the prosecution only, because the harm it guards against is wrongful conviction. Rebuttal. The threshold stays low. The Minister's account is that "once the defendant raises a real issue, the burden moves to the prosecution, which then has to satisfy the court beyond reasonable doubt that the computer is working accurately."

Most of the credit is elsewhere. Marshall and colleagues proposed a two-stage scheme in 2021: routine disclosure of known bugs, change logs, security standards and audits, then, if that reveals grounds for doubt, proof by the relying party that none of them might affect reliability, with the rule that "It should not be required that the party challenging the reliability of the data relied upon should identify the particular issue to which the disclosure required to be given is alleged to go." Their Stage 1 covers far more of what a system's owner knows than my tier's known defects. I add one narrow thing: a run-specific record and certificate as what disclosure contains, and a stated consequence for lacking them. The nearest rule in force that I have read is American. Since the 2017 amendments, US Federal Rule of Evidence 902(13) treats as self-authenticating a "record generated by an electronic process or system that produces an accurate result, as shown by a certification of a qualified person", and 902(14) does the same for data "authenticated by a process of digital identification", provided the proponent gives notice and makes "the record and certification available for inspection" (FRE 902). That is a tendered certificate with an inspection right, which is my shape. It differs twice: the certifier is a person attesting a process and not a checker recomputing one run, and the committee notes say a certification "can establish only that the proffered item has satisfied the admissibility requirements for authenticity". I have not surveyed others. That burdens should follow access is old, and I claim nothing new in it for law and economics; the Post Office pleaded it. My Make the Safe Harbour Compile has the same shape, a presumption earned by a decidable check, and Perfect Compliance, Defeated Purpose attacks it.

Even a perfect proof

Now give the proponent everything. In Ashdown the client withdraws consent at tick 5. The firm's specification takes withdrawal to bite when its register records it, at tick 8. At tick 6 the research agent reads the privileged advice. The record is true, anchored, certified and disclosed, and the opponent's own evidence confirms it. This compiles.

theorem perfect_evidence_wrong_rule :
    perfect.tender.record = perfect.run ∧
    Conforms perfect.spec perfect.run = true ∧
    finding .presumption perfect = true ∧
    finding .tiered perfect = true ∧
    rebutted perfect = false ∧
    right .tiered perfect = true ∧
    Conforms clientRule perfect.run = false ∧
    ValidOn clientRule perfect.spec probes = false := by decide

It is one computed case, and faithful_conforming_unrebuttable is the general form behind the thesis: on any dispute, a faithful record of a conforming run cannot be rebutted, whatever the specification says. The finding is right about the run, and the conduct breaches the rule above. Every improvement to the evidence helps the firm: the better the proof, the more firmly the wrong rule is shown to have been followed.

The real case is Robodebt, which Who Gets to Write the Specification? treats at length, and I add only one passage from the Federal Court of Australia. In approving a settlement, the Court said the materials indicated that the Commonwealth "maintained the Robodebt system in the face of approximately 29 decisions" of the tribunal, up to 30 May 2017, rejecting income averaging, and that the evidence showed it unlawfully asserted debts "totalling at least $1.763 billion against approximately 433,000 Australians" [(Prygodicz (No 2) [2021] FCA 634, [10], [4])](https://www.judgments.fedcourt.gov.au/judgments/Judgments/fca/single/2021/2021fca0634). The Commonwealth had admitted it had no proper legal basis for those debts. The question there was what the law required, and a certificate of faithful averaging would have been evidence for the wrong side.

no_review_of_the_dispute_settles_validity says that no function of the dispute equals validity against every possible rule. That is cheap: it holds because the rule above is not an argument of the function. So give the review the rule. two_readings_of_one_rule is the substance. "Consent ends when it is withdrawn" has two defensible readings, on notice and on recording, and the same specification is invalid on one and valid on the other. Formalising the rule above does not end the contest. It moves it to the reading, which is the subject of The Translator Writes the Rule and of what LegalLean says about Hart's open texture. The model holds two constants and does not choose.

At the top of any stack of checks sits something no checker supplies. On Hart's account as summarised by Green and Adams, the rule of recognition "specifies the ultimate criteria of validity in the legal system", and it "exists only because it is practiced by officials" (SEP, Legal Positivism). A kernel can tell you that a statement follows. It cannot occupy that practice, and a person contesting a rule is arguing inside it, by reasons a tribunal must answer. Lessig warned in 2000 that "This regulator is code", and that we would miss the regulation (Lessig, 2000). Citron warned in 2008 that automated systems "combine individual adjudications with rulemaking while adhering to the procedural safeguards of neither" (Citron, 2008).

What a forum must be able to do. forum_scope_decides computes it: the same decision stands in a forum that hears only the record and the run, falls in one that also hears the specification, and its certificate stays green either way. spec_ruling_reaches_every_decision is general, and it is nearly a definition: defects lists the specification as a ground against every decision under it once it fails on any probe, with no run examined. spec_ruling_overreaches shows the cost: a read at tick 2, lawful on either reading, falls too. Read it as the remedy the sixth packet field asks a forum to have, and not as a finding about any court. Severance, finality and relief for past decisions are not modelled. run_ruling_does_not_travel shows the contrast, on one pair of decisions.

UK law gives data subjects something here. Article 22C of the UK GDPR, inserted by the Data (Use and Access) Act 2025, requires safeguards that "enable the data subject to contest such decisions" (s.80). The text speaks of decisions. Whether contest there reaches the rule behind a decision I do not know.

The appeal packet

My own earlier essay needs a correction here. Who Gets to Write the Specification? proposed an appeal channel in which "an upheld appeal records that the system misapplied a valid rule", and a dispensation channel in which "a recorded override says the rule was applied correctly but should not have been", both counted and routed to the clause owner, with "Recurring upheld appeals" treated as "evidence the rule is invalid". Neither lets the person bound say that the rule is invalid. A count routed to the clause owner gives that question to the person defending the clause.

The artefact is a proposal; I know of no form like it. Packet.contestable is a decidable check over six fields:

1. the specification is published to the person bound;
2. the rule above it is named;
3. whoever adopted it is named;
4. a forum exists that hears the specification and authority grounds, and not only the run;
5. the challenge is still in time;
6. a successful challenge reaches past decisions under the same rule.

proof_only_packet_not_contestable gives the chapter's title as a computed case: a packet complete in every field, whose forum hears only the record and the run, fails, and with a full forum it passes. packet_expires shows it failing out of time.

The packet creates no new law, and tribunals and courts already exist. It supplies what a person needs to use them: which rule, whose rule, and where.

Thursday. A partner does not need Lean for this, or a product, and need not change how the firm practises. Pick one automated step whose output would be relied on against someone, a client included. Ask the supplier three questions in writing: which rule did it apply, who adopted that rule, and where could the person affected contest it? It costs an hour of unbilled time. The external date is the Law Commission's closing date of 14/01/2027, and the Rule Committee's rules are still unpublished. If the supplier cannot answer, the firm is relying on a rule it cannot explain to the person affected, and the partner who signs should know that. I sell into this market, so ask me the same three questions.

Who gets to use this. A Lean certificate is unreadable to almost everyone it could be used against. The call for evidence itself asks whether there are "sufficient such people" to act as experts. Tender formats favour repeat players, who can pay to produce them. A tier rule without funded independent readers would replace a blind presumption with an expensive one, and I have no costed answer.

Exists and proposed

Exists: the common-law presumption; the judgments, the 2024 Act and the Hansard record cited; the Law Commission's provisional proposals; Presumption.lean and its proofs. Proposed and not built: the tier rule and the appeal packet. Unresolved: how a court treats a statement it cannot read, who pays for reading it, and rebuttal when independent evidence is itself software output.

Objections

"Remove or weaken this and the courts stop." The Minister gave an estimate, with no source stated, that "90% of criminal cases involve the prosecution relying on some kind of computer evidence", most of it uncontroversial, and warned that companies abroad cannot be compelled to vouch for their systems. I cannot verify the figure, and the argument does not need it. Verdict: accepted against section 69's shape, and it is why the proposal is limited to software-generated evidence determinative of an issue. The tier adds no burden on a text message. Determinative output from a system nobody anchored must be proved by other means even with no real issue raised, and I accept that. I would change my mind if Rule Committee drafting showed that "determinative" cannot be applied before trial without satellite litigation in most cases.

"Horizon was non-disclosure, which the Ministry itself calls deliberate. No evidence rule stops a party determined to mislead." This is the objection I find hardest, and forged_record_earns_presumption is its theorem. Verdict: accepted for forgery, rejected for withholding. The enhanced disclosure the Government proposes may deliver most of the benefit. What the tier adds is a default that fails against the party holding the material, rather than a duty someone must detect has been breached. I would change my mind if disclosure rules alone, once in force, showed no pattern of unexamined software evidence over five years of appeals.

"You are building the next 'robust'. A certificate looks infallible." Fraser J records that the word robust "has been at the heart of the Post Office's defence of the Horizon system for many years". Verdict: accepted as the main risk. A certificate must be presented as a statement about a named record under a named specification, and perfect_evidence_wrong_rule is the warning label. I would abandon the tier if tribunals in practice treated a passing certificate as ending inquiry into the rule.

"Law is interpretive. Your packet turns a practice of giving reasons into a checklist of six booleans." Correct about the packet. Verdict: accepted, and the packet is limited accordingly. It decides whether a person can reach a forum, and nothing that happens there. I would drop it if filling it in became a substitute for the hearing, which is the Goodhart failure below.

Goodhart, and what is lost

Tie a presumption to a clean certificate and parties will prove weak statements, narrow the specification until it passes, and invest in clean records more than true ones. Packet.contestable reads what a forum is declared to hear, so a forum that has never upheld a challenge passes identically. So read the tier and the packet as premises to attack; the forum's record is for humans to read.

"A real issue" is the Minister's phrase for a threshold a judge applies, and my model turns it into a Boolean, losing a threshold that bends to the person in front of the court. Discretion to disbelieve a tidy record has no field in Dispute. The tier also risks teaching courts that disorganised evidence is suspect, and many honest small parties keep disorganised evidence. no_regime_dominates states that loss in one line.

Predictions

1. By 31/12/2027, the Criminal Procedure Rules for England and Wales will contain an express provision on computer-generated evidence, and no statute will have abolished the common-law presumption in criminal proceedings. Refuted by a statute abolishing it, or by no such rule being in force on that date.
2. The Law Commission's final product liability report, if published by 31/12/2028, will retain a rebuttable presumption of defect in some form and will give a defendant no route to displace it by tendering a specified form of machine-checkable evidence. Refuted by the published text. If no report appears by then, the prediction is untested and I will say so.
3. By 31/12/2029, no reported judgment of the High Court or above in England and Wales will rest a finding about what an AI agent did on a machine-checked proof certificate. Refuted by one such judgment. If this holds, the first half of this chapter stays speculative.

The second half does not wait on any of that. Build the proof, then tell the person it is used against where to take the rule.

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.