docs(release): truth-up formal coverage and closure handbook

Authority documents state the machine-checked coverage exactly: TLAPS
867/876 obligations with the nine unchecked lemmas named and classified,
the checked trace replay with its residual classes, the certified
compaction and fencing table, and the 31-job fast gate. The
broader-formal row remains open for both local residuals and the
external signature and attestation inputs; the decision remains No-go.

Author: metaphorics

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -7,12 +7,12 @@ This document explains the EPaxos and EPaxos Revisited behavior implemented in t
 The word "proof" in this repository means a combination of:
 
 1. source invariants in the Go implementation;
-2. finite TLC model checks for focused protocol slices plus a restricted arbitrary-history theorem over `tla/EPaxosInductiveProofs.tla`'s own abstract `ConcreteNext`;
+2. finite TLC model checks for focused protocol slices plus TLAPS checking of `tla/EPaxosInductiveProofs.tla`'s restricted `ConcreteNext` proof scripts, with 867 of 876 obligations proved, 9 failed, and 0 omitted;
 3. deterministic simulation tests, including deterministic state-transition (DST) scenarios;
 4. Go unit, fuzz, stress, and coverage gates; and
 5. local Jepsen harness evidence plus optional external validation tooling where separately exercised.
 
-This is not an unbounded mathematical proof of every possible EPaxos or Go execution. `tla/EPaxosInductiveProofs.tla` proves an arbitrary-history abstraction only for its restricted semantic `ConcreteNext`; it explicitly excludes codec, allocation, Ready ownership, SCC execution, TOQ timing, and other production transitions. `tla/EPaxosRawNodeRefinement.tla` remains an implementation-shaped finite workflow model, and no checked theorem connects that model or arbitrary Go `RawNode` executions to the inductive abstraction. The finite TLA+ models cover configured bounded state spaces. The executable Go refinement trace now validates semantic pre/post invariants and maintains a fail-closed exported-`RawNode` API inventory, but it is not a TLC/TLAPS replay of Go states against TLA action predicates. The current repository still names bounded non-claims: even-size optimized-quorum proof, arbitrary optimized-recovery network/message-loss/retry histories, recovery under reconfiguration beyond finite slices, operational synchronized-clock/one-way-delay implementation for TOQ deployments, arbitrary membership-change proof, in-place disk-corruption repair or synthesized reconstruction without a verified checkpoint, and target-environment mixed-version compatibility beyond the local loopback drill.
+This is not an unbounded mathematical proof of every possible EPaxos or Go execution. TLAPS 1.6.0-pre at version `763bf3c` proves 867 of 876 obligations in `tla/EPaxosInductiveProofs.tla`, with 9 failed and 0 omitted; `tests/tlaps_check.sh` is fail-closed and exits 10. The proved anchor families include initialization, normal proposal, recovery begin/evidence/proposal preservation, quorum intersection, and chosen-value recovery selection, but four isolated helper obligations and five unchanged original preservation lemmas remain undischarged. The module covers only its restricted semantic `ConcreteNext` and excludes codec, allocation, Ready ownership, SCC execution, TOQ timing, and other production transitions. The four-scenario Go-to-TLC replay checks a snapshot-only 12-variable abstraction against the model action predicates, and the exhaustive AST inventory classifies internal mutation/dispatch sites; together they prove sampled admission plus dispatch-site coverage, not arbitrary Go refinement. Residuals are unexercised `PaperObserveRecovery`, audited-but-unexercised `NormalValidationDrop/message-step`, 13 frozen bookkeeping variables, coordinator-and-designated-instance scope, and constant-abstracted `wire`. The current repository still names bounded non-claims: even-size optimized-quorum proof, arbitrary optimized-recovery network/message-loss/retry histories, recovery under reconfiguration beyond finite slices, operational synchronized-clock/one-way-delay implementation for TOQ deployments, arbitrary membership-change proof, in-place disk-corruption repair or synthesized reconstruction without a verified checkpoint, and target-environment mixed-version compatibility beyond the local loopback drill.
 
 ## 2. Primary paper obligations checked
 
@@ -522,8 +522,10 @@ Evidence: `examples/kv/cmd/kvnode/main.go`, `examples/kv/cmd/kvnode/main_test.go
 | `tla/EPaxosConfigRecoveryLostResponseRetry.tla` | One finite old-config recovery lost-response retry slice where removed-voter prepare and accept responses are explicit pre-retry losses, deterministic retry rebroadcasts remain pinned to old peers with old dependency width, and replacement responses after retry complete no-op recovery through the old 3/4 quorum. | Arbitrary recovery histories, arbitrary retry histories, arbitrary message loss beyond this named finite pre-retry loss shape, joint consensus, arbitrary membership histories, application output, and unbounded proof. |
 | `tla/EPaxosConfigAddRecovery.tla` | One finite staged recovery-after-addition slice where an old three-voter instance is recovered after the current config adds voter 4; added-voter prepare/accept attempts do not enter old quorum sets, old 2/3 quorum is sufficient, and the no-op executes. | Arbitrary recovery under configuration changes, joint consensus, message loss, arbitrary membership histories, and unbounded proof. |
 | `tla/EPaxosRawNodeRefinement.tla` | Four implementation-shaped finite normal, recovery, TOQ, and configuration workflows; bounded `RefinementProperty`, durability, Ready freezing, configuration pinning, evidence, execution order, and branch-coverage invariants. | Arbitrary Go execution refinement, arbitrary workflow composition, or an unbounded theorem. |
-| `tla/EPaxosInductiveProofs.tla` | Parametric arbitrary-history safety and `AbstractHistoryRefinement` for the module's restricted `ConcreteNext`. | Codec, allocation, Ready ownership, SCC execution, TOQ timing, the finite RawNode model, and arbitrary Go executions. No checked bridge theorem exists. |
-| `tla/EPaxosVoterBootstrap.tla` | Certified voter-bootstrap fence, target readiness, activation/abort, crash-prefix, and finite fairness obligations. | A RawNode refinement-trace workflow or a checked Go-to-TLA action simulation theorem. |
+| `tla/EPaxosTraceCheck.tla` | Four captured Go scenarios projected from semantic snapshots onto 12 refinement variables; each consecutive pair satisfies a model action predicate selected by its audited raw `(action, kind)` pair or exact 12-variable stutter. The atomic commit-plus-execute pair is a TLC-evaluated `PaperChoose`/`PaperExecute` relational composition; five negative controls reject. | `PaperObserveRecovery`, `NormalValidationDrop/message-step`, 13 frozen bookkeeping variables, non-coordinator/non-designated state, constant-abstracted `wire`, uncaptured executions, or an unbounded theorem. |
+| `tla/EPaxosCompactionFencing.tla` | Six compaction/fencing invariants over an ordered 11-state positive model with both lanes, both incarnations, and one fenced-configuration transition; six negative configs each trigger their exact invariant violation, with layered Go witness `TestFencingLayersRejectFoldedLoadAndStaleBootstrapAuth`. | Arbitrary compaction histories, unbounded uptime, or production storage-engine certification. |
+| `tla/EPaxosInductiveProofs.tla` | Parametric safety and `AbstractHistoryRefinement` statements for the module's restricted `ConcreteNext`; TLAPS 1.6.0-pre at version `763bf3c` proves 867 of 876 obligations, with 9 failed and 0 omitted. | Nine obligations remain unchecked; codec, allocation, Ready ownership, SCC execution, TOQ timing, the finite RawNode model, and arbitrary Go executions remain outside the module, and no checked bridge theorem exists. |
+| `tla/EPaxosVoterBootstrap.tla` | Certified voter-bootstrap fence, target readiness, activation/abort, crash-prefix, and finite fairness obligations. | Bootstrap is outside the sampled Go-to-TLC replay and there is no arbitrary-Go action simulation theorem. |
 | `tla/EPaxosRevisited.tla` | TOQ envelope, delayed assignment, pending-decision blocking, receiver processing, fast-wait behavior, and chain pruning. | Real clock synchronization and OWD measurement. |
 | `tla/TOQClockDiscipline.tla` | Finite bounded-skew/bounded-delay `ProcessAt` contract; in Go this maps to `TOQOneWayDelay` values that already include skew margin. | Operational clock-sync implementation or delay measurement. |
 | `tla/ReadyAdvance.tla` | Durable Ready/Advance prefix acknowledgement and retry. | Concrete storage engine behavior. |
@@ -566,7 +568,7 @@ The repository scripts wire focused verification:
 
 The implementation and evidence currently support a bounded library/example claim, not a mission-critical production-ready claim. The release remains no-go for the sole canonical item in `RELEASE_SCOPE.md`:
 
-- broader formal model coverage, including an unbounded Go/TLA refinement argument, checked action correspondence, and certified protocol-state compaction with late-message and incarnation fencing.
+- broader formal model coverage remains open for local reasons—the nine unchecked TLAPS obligations and the trace replay's five residual classes—and external reasons—independent producer/reviewer signatures and native-Darwin target attestation.
 
 Other target-environment, real-network, and operational properties remain explicit nonclaims rather than additional canonical release rows. Do not mark the active goal complete unless current evidence proves mission-critical production readiness and this remaining blocker is closed with direct evidence.
 
@@ -580,6 +582,6 @@ Observable evidence: focused Ready ownership/durability/capped-tail tests, 1..7
 
 The KV embedding has one lifecycle-owned logical-tick loop, proposal waiters, terminal error publication, atomic durable Ready application, capped-prefix frame admission, separate queue/retry capacities, and joined shutdown. Production mode requires mutual TLS 1.3 on peer, client, and admin planes. Peer certificates carry one replica URI SAN and inbound `Message.From` must match the authenticated replica. Client/admin CA membership is single-tenant authorization; per-user and multi-tenant RBAC are not implemented.
 
-Pebble resource options and storage counters are explicit. Retention thresholds stop new proposals at pressure and stop all protocol mutation at the configured limit, but never delete instance history. This is a finite retention horizon, not certified compaction or unbounded uptime.
+Pebble resource options and storage counters are explicit. Retention and compaction may fold a contiguous durably executed prefix, remove folded records from resident state while retaining durable authority, and drop executed payload capacity while preserving checksum and decided-tuple authority. `tla/EPaxosCompactionFencing.tla` certifies six named requirements only in its ordered 11-state scope, including singular decision-preserving late-message reload and stale-incarnation/closed-configuration fencing. This is not a proof of arbitrary compaction histories or unbounded uptime.
 
-- Evidence consists of tagged KV behavior and race tests, deterministic fault simulation, and bounded finite model checking. Current evidence is limited to Darwin arm64, three-node same-host loopback service exercises, and simulated network faults. It does not provide unbounded formal proof, certified protocol-state compaction, real-network fault evidence, or a mission-critical production-readiness claim.
+- Evidence consists of tagged KV behavior and race tests, deterministic fault simulation, bounded finite model checking, the five-control sampled Go-to-TLC replay, and partial TLAPS checking with nine failed obligations. Deployment/service evidence is limited to Darwin arm64, three-node same-host loopback exercises, and simulated network faults. It does not provide an arbitrary-Go refinement theorem, production storage-engine compaction certification, real-network fault evidence, independent producer/reviewer signatures, native-Darwin target attestation, or a mission-critical production-readiness claim.