An Emergency Stop Is Not an Abort: A Third Teardown Verdict, a Shared Kill-Switch Latch, and a Mechanized Accounting of What Is Left Owed

Pitch

An operator emergency stop is a third verdict next to commit and abort: it replays nothing, drops nothing, names the one crossing that may or may not have landed, and a Lean-checked disposition table proves every registered obligation is on exactly one book.

Abstract

Systems that run effectful agent or service compositions usually offer two ways to end an activation: commit, which discharges its undo obligations, and abort, which replays inverses in reverse order. Both are cooperative. When an operator hits the button during a runaway loop with irreversible effects in flight, unwinding hundreds of brackets is a long answer, and every inverse is another chance to cross the boundary again. We describe the operator E-Stop in revl, a language whose compiler derives teardown from declared inverses. The E-Stop is a third verdict, halted. A latch file, read by the same rule in every honoring runtime, makes each seam that dispatches or accepts a boundary crossing refuse new work, including when the latch is malformed. In-flight work is reported as ambiguous, never guessed, and a halted child prints an inventory and dies without a graceful-teardown claim. The Lean development extends the existing LIFO completeness and soundness theorems to the new verdict: the completeness theorem needs no new hypothesis, two corollaries gain an explicit settling hypothesis, and it proves that every (entry kind, verdict) pair is exactly one of replayed, discharged or stranded and that the three books partition the stack under every verdict. The design deliberately gives up the no-residue property of abort and replaces it with "all residue, all of it reported". The py runtime and the go, rust and java placement runners honor the latch today; node and wasm do not yet, and the conductor reports them by name as killed with residue unknown. We have no latency or fault-injection measurements yet.

Problem and claim

Existing stop mechanisms fall into two families. Cooperative ones (supervisor shutdown, drain, saga compensation) run more code at the worst moment. Hard ones (SIGKILL, a feature-flag kill switch) stop fast but leave no account of what is owed, and a flag only protects the call sites that read it. Neither says which obligations remain and which single operation may have landed.

Claim: an emergency stop is a verdict in its own right, with a total accounting, not a faster abort. The design doc states the trade directly: "An E-Stop trades resource cleanliness for stop latency" (docs/design/443-estop.md). Four guarantees are given and no more: bounded latency (no new crossing once the latch is set), nothing invented (zero inverses, compensations or flushes run), total accounting, and at most one ambiguous crossing per activation. It also lists what it does not give: no G7 LIFO completeness (vacuous), no R4 no-residue, no handle release.

A second claim concerns uniformity: the latch rule, including fail-closed on a malformed or unreadable latch, is reimplemented byte-for-byte per tier (src/revl/estop.py, backends/typescript/estop.ts, the go, rust and java twins), so tiers cannot drift on what an armed latch means. The evidence supports four honoring tiers (py, go, rust, java), not five runtimes; see below.

Contributions

1. A third teardown verdict halted with a stranded disposition (registered, not run, not dropped, keeps inverse and witness), and the rule that a halt is shaped like a crash so revl recover reconciles it (docs/design/443-estop.md, "Open question 3").
2. A Lean extension: G7 completeness and soundness hold for .halted unchanged with an empty replay set; the disposition trichotomy and the book-length partition hold under every verdict; two corollaries gained an explicit settles hypothesis, shown load-bearing by counter-instance and by an equation with no hypothesis (bracket_replays_exactly_when_settling).
3. A one-latch cross-tier protocol (contract E1 to E8 in docs/design/443-estop-tier-contract.md): one reader rule, every seam consults it, unarmed is free, an in-flight registry, one inventory line, an idle watcher, die where it stands, no self-halt.
4. A multi-process conductor that distinguishes populations (honoring tiers, no-seam tiers killed with residue UNKNOWN, static wasm) and counts UNKNOWN lines in the residue total, so the report is incomplete by exactly the processes it names.
5. An authority model: estop is its own operator verb, subject-scoped over the whole running composition, with no in-language surface, and runtime.estop() refuses without an operator token.
6. A halt is seen by other processes as peer death, not as a halt: consumers of a halted provider unwind gracefully by the existing R2/R3 rules.

Related work

Evidence on main

Numbers that exist

• 18 formal-status rows tagged "G7 / item 443" (formal/STATUS.md). docs/design/443-estop.md says only that four further theorems pin the settling hypothesis.
• Test counts per file are listed above (29, 9, 8, 7, 6, 3). No latency, throughput or fault-injection numbers exist. REVL_ESTOP_HALT_WINDOW defaults to 2 s (docs/design/443-estop.md, conductor section); that is a configured bound, not a measurement.

Paper outline

1. Introduction: the stop nobody models; commit, abort and what an operator actually needs.
2. Background: derived LIFO teardown, G7, R4, the WAL and revl recover.
3. The halted verdict: table, four guarantees and three non-guarantees.
4. Mechanization: trichotomy, partition, the settling hypothesis made load-bearing, the halt cut and at-most-one ambiguity.
5. One latch, many runtimes: E1 to E8, fail-closed, unarmed-free, seams, idle watcher.
6. The conductor and honest reporting of populations (honoring, killed, static).
7. Authority: operator verb, no in-language surface, peer-death semantics.
8. Evaluation: latency, fault injection, conformance across tiers.
9. Related work, limits.

Threats to validity and limits

• The docs say the unwinding trade is real: handles, connections and leases stay held until exit or recovery. Brackets are closure-only on every tier, so recovery reports them as unreconstructible ("What stays open" in the tier contract).
• The formal layer is tier-independent and proves accounting over a model of the stack; it does not prove that any runtime's seams cover every crossing path. Issue #1504 shows a real miss that was fixed by test, which is evidence against claiming completeness.
• "Bounded latency" is a design property with a configured 2 s inventory window, not a measured one.
• The node tier "kept dispatching crossings until it died" under a placement halt (report text in docs/design/443-estop.md); wasm is static. A reader must not read "five runtimes" as uniform enforcement.
• A halted provider is seen as peer death by consumers; a halt does not propagate. Remote tasks on peers keep running (tier contract, "What stays open").
• The latch is a file: a hostile process with write access to the directory can arm it (denial of service) or remove it before a watcher reads it. The docs call the missing control socket a deliberate choice; no threat analysis exists.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 17 checked, 4 corrected.

Cite this draft

@misc{revlp25,
  author       = {Thomas Moussajee},
  title        = {An Emergency Stop Is Not an Abort: A Third Teardown Verdict, a Shared Kill-Switch Latch, and a Mechanized Accounting of What Is Left Owed},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P25.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.