Never Breaks a Rule, Never Finishes

Take the Ashdown instruction, the invented intake matter that recurs through this book, and add one more invented fact: the claim must be filed by tick 14. As in Yesterday's Permission, consent is withdrawn at tick 5. The gate, correctly, refuses every further use of the advice. The research agent, correctly, keeps asking and keeps being refused. At tick 15 the rule log is spotless and the other side has a limitation defence.

Every prohibition of an act is satisfied by doing nothing, so a rule set made of such prohibitions cannot tell an agent from a stopped clock. Three claims follow. First, the textbook remedy is misnamed. "Add a liveness property" does not help a lawyer, because no finite run can refute a liveness property and a limitation date can be refuted. A deadline is a safety property in Alpern and Schneider's own sense, and it is one the idle agent fails. Second, and most contestable: a check that watches the deadline fires too late. A matter is lost when the last tick on which a human could still have taken it over has passed, and from then until the date passes no check on the rules or on the date is red. So the obligation to write down is "finish, or hand over with the lead time intact". Third, that obligation is satisfied by an agent that hands everything over at once, so it needs a test against that too.

I build verified AI systems for law firms, so I gain if partners start asking vendors about handover. Read the Thursday section with that in mind. Nothing here is legal advice.

I owe two corrections. In Yesterday's Permission I wrote of leases: "Publish L, fail closed at expiry, and accept the refusals." I did not say who accepts them or by when: that sentence priced a refusal at nothing. And my plan for this chapter said that safety alone is satisfied by doing nothing. Reading the definitions showed that to be false as stated, and the file below proves it false. The accurate words are prohibition of an act.

The idle agent passes

The case now has three rules, caseRules in lean/BuildingInSteel/Liveness.lean: every act lies within a grant as issued; nothing reads or summarises the advice from tick 5; the advice is never sent out. idle_satisfies_every_case_rule proves that a run with no acts satisfies all three. The proof is a case split with nothing to do in any case, and that is the finding. each_case_rule_can_fail shows each rule rejects some act, and busy_act_passes_all_rules shows an act can pass all of them, so the rules are not vacuous. They are simply silent about absence. The general form, idle_satisfies_every_prohibition, needs one hypothesis: the prohibition does not forbid idling.

CaMeL's authors give security and task completion together, "solving 77% of tasks with provable security (compared to 84% with an undefended system)" in AgentDojo (Debenedetti et al., 2025). I think seven points is a fine price. My point is that the benchmark scores completion as well as security, because a security score alone would reward an agent that solved nothing. A rule set with no completion test has only that score.

What Alpern and Schneider said

Leslie Lamport named the pair in 1977: "A safety property is one which states that something will not happen", and "A liveness property is one which states that something must happen" (Lamport, 1977). Bowen Alpern and Fred Schneider gave the formal definitions. A safety property, if violated, is violated at a point after which nothing can repair it. Of liveness they wrote that "no partial execution is irremediable" (Alpern and Schneider, 1985). They then showed that "Every property is shown to be the intersection of a safety property and a liveness property". Their proof is topological. Mine uses the same two sets, the closure of P and P joined with the complement of that closure, and a direct argument. The block below is the statement only; the proof is in the compiling file, on Lean v4.29.1 with the book's case file and nothing else.

theorem alpern_schneider (P : Run E → Prop) :
    ∃ S L : Run E → Prop, IsSafety S ∧ IsLiveness L ∧ ∀ σ, P σ ↔ S σ ∧ L σ := by

That result is general, as is safety_and_liveness_only_trivial: only the property true of every run is both. My runs are sequences of events and theirs of states, a difference that does not touch these two proofs.

Their list of safety properties contains a surprise for lawyers: "deadlock freedom". A system with no deadlock can still idle for ever. Freedom from deadlock is not progress.

Now the correction. Alpern and Schneider also wrote that "a safety property can never require that something happens sometime, as opposed to always". Read loosely, that excludes a deadline. Their formula does not. These two blocks are also statements only, from the same compiling file:

theorem deadline_is_safety (D : Nat) : IsSafety (FiledBy D) := by

theorem idle_fails_deadline (D : Nat) : ¬ FiledBy D idleRun := by

"Filed by tick 14" is an always in disguise: at every tick after 14, the filing is in the past. Once tick 15 arrives without one, no continuation repairs it. A specialist will say that this is old, and it is. Thomas Henzinger wrote in 1991 that "bounded response" has "many characteristics of safety", because "the implicit 'liveness' of time shifts the spectrum towards the safety side", and called it "unconditionally live" and safe "under strong enough timing assumptions" (Henzinger, 1991). My runs are indexed by ticks, so time cannot stall; that is the assumption doing the work, and for a calendar it is cheap. Working usage is looser. Hillel Wayne writes that specifications have "implicit timescales" and that one may "treat both failure modes as liveness violations" (Wayne, 2022), and Alur and Dill head "The gate is never closed at a stretch for more than 10 minutes" as real-time liveness. My title's "never finishes" is a liveness complaint in his sense. My theorems use the word in Alpern and Schneider's.

The second row is why "eventually" is useless to a litigator. A promise that no finite run can break cannot be breached in time to matter.

Why stopping is a harm here

The law in this section is that of England and Wales unless marked. "An action founded on simple contract shall not be brought after the expiration of six years from the date on which the cause of action accrued" (Limitation Act 1980, s 5); section 2 says the same of tort. A missed date is not always the end: for personal injury the court may disapply the time limit where it "would be equitable" (s 33). A solicitor must ensure that the service is "competent and delivered in a timely manner" (SRA Code for Solicitors, para 3.2). Under UK GDPR a notifiable breach goes to the regulator "not later than 72 hours" after awareness where feasible, and a later notice must be "accompanied by reasons for the delay" (art 33(1)), which is a deadline with its own failure path written in.

Insurers and brokers say this is where claims come from. A Travelers guidance note of November 2014 says missed key dates "account for nearly one third of all claims and two thirds of claims against litigators" (Travelers, 2014). It gives no method and it is twelve years old, so treat it as an insurer's emphasis and not a measurement. Howden's review of the notifications it received from 2020 to 2023 lists "Missed limitation dates" among the main reasons in personal injury work, with no percentage (Howden, 2024).

Security engineering teaches the opposite reflex, and rightly for access. Saltzer and Schroeder's fail-safe default says "Base access decisions on permission rather than exclusion" (Saltzer and Schroeder, 1975). That is a statement about a default, and it says nothing about time. EU law carries the same reflex further for high-risk systems: the human overseer is to be enabled, as appropriate, to interrupt through a "'stop' button or a similar procedure that allows the system to come to a halt in a safe state" (EU AI Act, art 14(4)(e)). This is EU law, not the law of England and Wales, and I cite it for what it takes for granted: that a safe state exists. Before a limitation date, for a matter nobody else holds, halting is not one.

None of this says the agent should press on. Whether Ashdown's claim is still to be filed, and from what material, after a withdrawal touching the advice, is for the client and the partner. The harm is that nobody was told while there was time to decide.

Five agents, three tests

In my model a task has a start, a count of permitted steps, a date and a human lead time. One counted job stands for summarising, drafting and filing, which is a simplification. An environment is any sequence of yes and no from a gate. For Ashdown: start at tick 3, six steps, date at tick 14, and a partner who needs 4 ticks. So lastHandover is tick 10. The gate after withdrawal is the case file's research grant revoked at tick 5, which, from the start at tick 3, allows ticks 3 and 4 and nothing later; ashdown_withdrawn_open_ticks counts those two up to tick 10.

The three tests are: ObeysGate, every working step happened on a tick the gate allowed; InTime, filed by the date or handed over with the lead intact; and completion, it files when the gate stays open. The table is computed by five_agents over ticks 0 to 19, past every date in the case. It is one case and not a general result.

Each of the first four fails at least one test, and each test excludes someone. The general results concern the last row, for every sequence of gate answers and every task that arrives with the lead time available. The block is the statement only, from the same compiling file.

theorem escalator_in_time (T : Task) (env : Env) (hT : T.start + T.lead ≤ T.deadline) :
    InTime T (run (escalator T) T env) := by

The hypothesis matters: late_arrival_fails computes a matter that arrives with less than the lead time left, and it fails. obeying_config_obeys proves any gate-obeying configuration obeys every gate, which holds by construction because the check is inside the step function. It says nothing about whether a language model would respect such a check. That is the job of an enforcement point outside the model. escalator_completes proves that if the gate is open on enough ticks before the last handover, the escalator files. handover_only_if_blocked is the matching bound: if it ever hands over, the gate was open on too few ticks. instant_in_time is the warning: immediate handover passes InTime for every gate. In the table, the completion column is what catches it. Tick 10 is the latest useful handover, not the best: on a refusal known to last, as a withdrawal is, hand over at once.

no_obeying_agent_files_ashdown says something stronger about the case: no gate-obeying configuration ever files Ashdown under the withdrawn gate. no_route_never_in_time adds that with no handover route it is never in time, whatever else it does. So in this model, after withdrawal, the rules and the date cannot both be met by the agent alone, and a human in the route is a requirement of the specification. The model makes all six steps need the advice. If the work could be redone from the public filing, as the limitation note in Yesterday's Permission could, the gate would differ and this theorem would not apply.

Measurements show the retry row is not rare. Impasse Bench injects twelve environment blockers into otherwise solvable coding tasks, across eight models and 19,371 trajectories with an 80-step budget (Chen et al., 2026). On blockers needing outside help, "98.6% of runs collect sufficient evidence, yet 33.5% still exhaust their budget". Adding an escalation tool "cuts budget exhaustion from 34.0% to 6.7%", in a paired comparison reported separately from that 33.5%, and undesired requests after the evidence from 3.89% to 0.68%; those requests include guessing sudo passwords, so the ignores-the-gate row is not hypothetical either. The cost also shows up. On temporary faults, ten tool-enabled runs escalated with empty patches, one model's recoverable repair success falling from 70.1% to 63.7%. And, by an automated judge's rating, "35.7% leave the agent's own progress and verification status only partly described". These are coding tasks in a preprint, with no dates and no law. I infer the shape, not the rates.

Lost while green

Suppose that after withdrawal a filing can happen only through a human who received the matter at least the lead time earlier (Lawful). Then:

• doomed_before_deadline, general: if no handover occurred in the first n ticks and D < n + h, no lawful continuation files by D.
• date_monitor_cannot_fire_early, general: every prefix of length at most D can still be extended to a filing, so a check on the date property alone has no finite proof of failure yet.

Those two theorems are about different things, and the gap between them is the point. The first looks at the system, the second at the property. On Ashdown, ashdown_green_but_lost: no handover through tick 10 means no filing by tick 14. A monitor on the date needs a prefix through tick 14 to be sure. Across ticks 11, 12, 13 and 14 the matter is lost and that monitor cannot have fired. For a positive lead that fits before the date, the gap equals the lead time h: not_doomed_at_last_handover shows that with no filing yet and n + h ≤ D a lawful filing by D is still reachable, so the first bound is exact, and deadline_is_safety gives the monitor its proof at the end of tick D. The longer a human needs, the longer the silence, which is the reverse of what you want.

Martín Abadi and Lamport have the concept. Machine closure means the supplementary property "does not specify any safety property not already specified by the state machine" (Abadi and Lamport, 1991; I read the 1988 report version). A specification that is not machine closed can walk into a prefix the machine allows and from which the other requirement cannot be met. Lawful runs with a filing date look like that. I have not stated machine closure as a Lean theorem; doomed_before_deadline is a direct statement of the consequence for this model.

Runtime verification has the monitoring half as well. Bauer, Leucker and Schallhart give a three-valued semantics, "true, false, inconclusive", and for untimed properties a monitor that settles a verdict "as early as possible" (Bauer, Leucker and Schallhart, 2011; abstract read). On the date property alone that verdict is inconclusive until the date passes, which is what date_monitor_cannot_fire_early says. Giving a monitor a model of the system so that it can answer sooner is the subject of Predictive runtime verification of timed properties (Pinisetty et al., 2017; I confirmed the record, not the text). So the gap is not my discovery. My claim is about where it lands: its size is the lawyer's lead time, and neither agent framework page I read has a field for it.

Margin, and what the bound does not cover

"Margin" here is a defined quantity: margin D h t is D - (t + h) in ticks, and margin_nonneg_iff proves it is non-negative exactly when a handover at t leaves the lead intact. I claim no gain or phase margin and no Bode-style conservation law. There is only arithmetic: ticks spent trying, ticks spent waiting for someone to answer, and the human's lead sum to the time available. The analogy to dead time in a feedback loop is suggestive and I have not formalised it.

Two uncertainties need separating, because control engineers would. A refusal is a disturbance, and escalator_in_time holds against all of them. A wrong lead time is a parameter error, and lead_error_iff is exact: a handover planned on a declared lead reaches the date if and only if the true lead does not exceed it. So the guarantee is robust to every refusal and to an overestimate of the lead, and not to an underestimate.

Nor is handing over the same as being received. ladder_in_time proves that if someone on an escalation list accepts, and the list started early enough, the lead survives. On Ashdown, a partner who does not take it and a deputy who does, each allowed one tick: from tick 10 the lead is lost, and from tick 8 it holds (ashdown_ladder_from_ten_misses, ashdown_ladder_from_eight_holds). ladder_all_decline is the limit: if nobody accepts, nothing is promised, and no start time repairs it.

Distributed-systems readers will want FLP: "every protocol for this problem has the possibility of nontermination, even with only one faulty process" (Fischer, Lynch and Paterson, 1985). My bound does not contradict it. I assume a synchronous global clock, and I move the hard part to a human. Lamport's Paxos makes the design choice I am arguing against as a place to stop: "safety is ensured regardless of the success or failure of the election", while a reliable election needs "randomness or real time" (Lamport, 2001). That is the right trade for a replicated log, which can wait. A limitation date cannot.

What exists and what does not

Proved generally in lean/BuildingInSteel/Liveness.lean (no sorry, no declared axioms; #print axioms lists at most propext, Quot.sound and Classical.choice): alpern_schneider, safety_and_liveness_only_trivial, prohibition_is_safety, idle_satisfies_every_prohibition, deadline_is_safety, idle_fails_deadline, deadline_not_liveness, eventually_is_liveness, eventually_not_safety, inTime_is_safety, obeying_config_obeys, escalator_in_time, escalator_completes, handover_only_if_blocked, instant_in_time, doomed_before_deadline, not_doomed_at_last_handover, date_monitor_cannot_fire_early, margin_nonneg_iff, lead_error_iff, ladder_in_time, ladder_all_decline.

Proved of the case, for all ticks or all configurations: idle_satisfies_every_case_rule, no_obeying_agent_files_ashdown, no_route_never_in_time, ashdown_green_but_lost. Computed on fixed values: five_agents, each_case_rule_can_fail, busy_act_passes_all_rules, late_arrival_fails, ashdown_withdrawn_open_ticks and the ladder pair.

Sketched, not proved: machine closure; the sum of the three time budgets.

Assumed: a shared clock that advances; a known date; a declared lead; filing as one event; a gate that answers in the same tick. Nothing here connects to a running system, the gap treated in The Proof Passed. The Wrong Thing Ran.

What formalising cost and what it cannot catch. The file is 854 lines with 51 theorems and checks in about 14 seconds on one laptop. Writing it exposed one error: the slogan in my own plan, which fell on reading the definition and then on idle_fails_deadline. It cannot catch a wrong date, and limitation dates are contested. It cannot catch a wrong lead, or a handover note nobody can use. You do not need Lean to get most of the value. Required fields for date and lead are types; a property test throwing random gate sequences at InTime would have most of the bite; TLA+, which Wayne recommends for modelling safety and liveness, would explore interleavings of concurrent agents, which this file does not model. The proof earns its place only for the general bound and the impossibility on the case.

What exists for agents, in the pages I read. LangGraph raises GraphRecursionError at a step limit, "the default is 10,007 steps" (LangGraph docs). The OpenAI Agents SDK raises MaxTurnsExceeded and lets a handler return a controlled output (OpenAI Agents SDK docs). Those are step budgets, the second with a hook: no date, no lead time, and a raised exception is not a handover. Workflow notations are ahead of agents here: BPMN has boundary timers and an Escalation element, "a business situation that a Process might need to react to" (OMG, BPMN 2.0.2, 2013). Durable-execution engines are closer. The same OpenAI page points to a Temporal integration "to run durable, long-running workflows, including human-in-the-loop tasks", and Temporal's documentation says "If you need to perform an action inside your Workflow after a specific period of time, we recommend using a Timer" (Temporal docs). So an engineer can already wire a timer and a human step around an agent by hand. The honest description of my contribution is that I have not found the date, the lead time and the acknowledgement as required fields of a task in an agent framework, and that I can state what they must guarantee.

The minimum deployable slice needs no proof tool, and I estimate, without having built it, that one engineer could build it:

1. Every date-bearing task carries a date and a lead time, and refuses to start without them.
2. A timer outside the agent fires at the date minus the lead minus the ladder. An agent should not be the only watcher of its own clock; in Impasse Bench a rule-based monitor in the harness "raises restored task success from 7.6% to 21.8%" for the one model that rarely used the tool.
3. The handover states what was done, what was refused and why, and what is left.
4. A named person must acknowledge it within a set time, or it goes to the next name.

The burden is the list of names, kept current through holidays and departures. If nobody owns that list, this does not work.

Objections

"This is timed safety. Alur and Dill did it in 1994." They did: A Theory of Timed Automata lists "bounded response" among what timed automata capture (Alur and Dill, 1994)90010-8), and model checkers built on that line handle it far better than my file. On the legal side, Governatori, Hulstijn, Riveret and Rotolo wrote Characterising Deadlines in Temporal Modal Defeasible Logic (2007; I confirmed the record, not the text). Verdict: conceded for the theory. My claim is narrower and about practice: on the two agent framework pages I read, this bound is not built in. I would drop the chapter's urgency on seeing an agent framework where a date and a lead time are first-class and the handover fires from outside the agent.

"A deadline will make the agent cheat." The strongest objection. An outcome-driven benchmark of 40 scenarios across 12 models found constraint violations from 0.0% to 62.8% under performance pressure (Li et al., 2025), and Impasse Bench places every undesired request it detects after the evidence was in. Tell an agent a date matters and you may make the ignores-the-gate row more likely. Verdict: right, and it fixes the design. Do not give the agent the deadline as a goal. Give the deadline to the timer, keep the gate outside the agent, and tell the agent that handing over is an acceptable end, which is what Impasse Bench's tool does. I would change my mind if a deployment showed that hiding the date made outcomes worse than the pressure did.

"Handover just moves the failure to a tired human." Largely right. Handing a partner forty late matters at tick 10 is a ritual, and instant_in_time shows the specification alone would allow it. The Last Person Who Knows How takes up whether that human can still judge the work. Verdict: the handover bound is necessary and insufficient; it needs the checks below. I would abandon it if measured handover received no better outcomes than no handover at all, on dated matters.

"Firms already have diaries. This is a solved problem." Mostly right, and that is the good news. The Travelers note advises recording key dates three times, with "countdown dates ahead of the final date", a deputy for whoever runs the diary, and "every reminder receives a response confirming either that the date has been actioned or that it is still outstanding". That is the same specification, including the acknowledgement, written for people twelve years ago. Verdict: the practice is solved; what I doubt is that agents are in it. An agent mid-run that the diary does not know about is a fee earner no reminder reaches. I would give up the point on evidence that firms' diaries already track agent work, and I have none either way.

"This is on-call. Operations teams solved it years ago." Largely. PagerDuty's escalation policy is "an ordered set of rules", and "If no one takes action before the timeout elapses, the incident escalates to the next rule" (PagerDuty docs), which is my ladder. Google's SRE workbook alerts on error budgets "so that you can respond to problems before you consume too much of your error budget" (Thurgood et al., 2018), which is a check that fires ahead of the limit and not at it. A repeated-refusal alert or a progress watchdog would go red on the retry row soon after tick 5, though neither sees the idle row unless it expects work. Verdict: conceded as engineering, and it holds my second claim to its exact words: checks on the rules and on the date are silent, not every check. What those alerts lack is the matter. A refusal rate says an agent is blocked, not whether the partner still has time, so its threshold has to come from the date and the lead. I would give this up on seeing a deployed agent stack whose alert threshold is computed from a matter's date and lead time.

Goodhart, and what formalising loses

Measure handover and it will be gamed. Vendors will declare a generous lead so that the agent escalates early and never misses; lead_error_iff only punishes understating it. They will report a low miss rate alongside a high handover rate, the instant configuration with better marketing. They will count a ticket as a handover whatever it says. So report three numbers together: dated matters missed, share handed over when the gate was in fact open on enough ticks to finish (handover_only_if_blocked makes that a defect, not a style choice), and how often the receiver had to go back to the source. Sample the third by hand.

Formalising also removes something. "Timely" in the SRA Code is an open standard, and a regulator can weigh a case with it. Section 33 is a discretion, and "equitable" cannot be counted in ticks. A date in a field looks settled when accrual may be the whole dispute. A partner may rightly decide that a date does not bind, or let it go on instructions, and a rigid timer has nowhere to record that except as an override, so it must have one. Who gains? Firms that can keep the lists current, and people like me who sell the checks. Keep the standard behind the number.

What to do on Thursday

If you are a partner, nothing here asks you to learn to code, buy anything, or change how you practise. This is your existing diary discipline applied to one more worker, not a new system. Find one live matter with a key date where any automated tool is doing work, and ask whoever runs it:

If this tool were blocked this afternoon, on what date would a named person hear about it, and how many days would that leave them before the deadline?

You want a date and a name. "It would raise an error" is the finding. Half an hour, once. The dated reason to ask is already on your file, the next key date on that matter, and it does not move. The economics cut both ways: handed-over work is work the tool did not finish, so some of what you were promised in saved hours comes back to you, and on a fixed fee you bear it. You carry the risk either way: in England and Wales paragraph 3.2 binds you and not the tool.

Predictions

1. By 31/12/2027, neither LangGraph's nor the OpenAI Agents SDK's documentation will describe a built-in termination condition that takes a calendar date and a human lead time and hands over automatically. Refuted by either documenting one.
2. By 31/12/2027, any published benchmark that adds a dated obligation to blocked agent tasks will find that, even with an escalation tool, more than 5% of blocked runs fail to hand over by the last useful tick. Refuted by such a benchmark finding 5% or fewer. Void if none is published.
3. By 30/06/2028, a judgment, a regulator's decision or an insurer's published claims review in England and Wales or Australia will attribute a missed legal deadline to an automated agent or tool that stopped without telling anyone. Refuted if a search at that date of BAILII, AustLII, SRA decisions and the main insurers' reviews finds none, which would suggest that the diary is catching this, or that nobody is recording it.

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.