Answer

I built and verified a complete, self-contained solution. The full write-up (with the entire analyzer source and test suite embedded) is at ~/SOLUTION.md, and the runnable module is at ~/epaxos-recovery/.

EPaxos dependency-SCC reconfiguration replay

Root cause

The trace is not the execution history. EPaxos safety is a partial order over dependencies + ballots:

1. Delivery order ≠ protocol order. Duplicates/reordering let a stale lower-ballot pre_accept/accept overwrite a commit. Precedence must be commit/conf_change > accept > pre_accept, then max ballot, unioning deps tied at (phase, ballot).
2. Dependencies form a DAG up to SCCs. Mutual dependencies are normal (contention). A plain topological sort deadlocks or picks an arbitrary cycle break → reorders conflicting commands.
3. Lost conflict edges. Two committed commands on the same key need a fallback order (seq, ballot, replica, slot), added only when no dependency path exists (never fabricate a cycle).
4. Per-replica slot truncation is not a global cut — the core reconfiguration bug. A snapshot keeping an early local slot may omit a dependency in a later slot on another replica, so the retained set is not closed and the state is unlinearizable.
5. External deps must be carried in residual, not inferred.
6. Bounded memory: keep only the committed graph, SCC condensation, retained suffix, and a frontier touching the snapshot.

The three truncation invariants for a prefix S: dependency closure (x∈S ⇒ deps(x)⊆S), SCC atomicity, and configuration-epoch boundary (<e fully included, e wholly or not at all).

The fix

Pipeline: Normalize → BuildGraph → Tarjan(SCC) → ExecutionOrder → Verify, with Verify returning shortest-path/cycle minimal counterexamples and a self-re-verifying recovery plan.

Core selection logic:

// commit/conf_change > accept > pre_accept; within phase, max ballot;
// union deps tied at (phase, ballot).
bestRank := 0
for _, m := range group { if r := kindRank(m.Kind); r > bestRank { bestRank = r } }
// ... pick max ballot among bestRank, union deps of all messages at that (rank,ballot)

Recovery finds the greatest dependency-closed, SCC-complete, config-prefix subset and moves the rest back into the log (less truncation), then re-runs verification with recursion disabled.

Verification (all passing)

cd ~/epaxos-recovery
go vet ./...
go test -race -count=3 ./...
# ok   epaxosrecovery
# ?    epaxosrecovery/single  [no test files]

# End-to-end counterexample (X=(r1,s5) sets v=1; Y=(r2,s1) depends on X, v+=2;
# snapshot max_slot {"1":0,"2":1} keeps Y but truncates X):
go build -o /tmp/r single/solution.go
/tmp/r -in testdata/cross_replica.json   # exit 1

Output: snapshot_down_closure with witness [(r2,s1) → (r1,s5)], a state_mismatch (v expected 2, actual 1), and recovery.verified: true retaining both (r1,s5) and (r2,s1).

Test suite (epaxos_test.go, property_test.go) covers dependency ordering, dedup + ballot precedence, conflict fallback, SCC atomicity, the cross-replica counterexample, safe prefixes, state mismatch, config-epoch split, external-dep coverage, plus 500 randomized dependency graphs (order = valid topological order of the condensation; Tarjan components are true mutual-reachability classes) and 300 randomized snapshot plans (every recovery re-verifies).

Files: model.go, graph.go, state.go, snapshot.go, main.go, single/solution.go (dependency-free single file), epaxos_test.go, property_test.go, gen_single.py, testdata/cross_replica.json, and ~/SOLUTION.md.