diff --git a/.github/workflows/README.md b/.github/workflows/README.md
index c7b21e10465..e2e92c17529 100644
--- a/.github/workflows/README.md
+++ b/.github/workflows/README.md
@@ -114,6 +114,11 @@ and the proof implementation files marked as generated for review purposes.
 The standard `mk_all --check` command ensures that the audit root imports every
 library module, so newly added proofs cannot silently escape the checks.
 
+The trace-validator job builds and audits the isolated strict trace validator,
+then runs its parser, replay, extraction, and ordering checks. The Milan and
+Genoa SNP jobs in `ci.yml` validate real committed C++ recovery traces and
+upload the original node logs consumed directly by Lean.
+
 File: `lean.yml`
 3rd party dependencies: None
 
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e0ff26ae876..c5804478ab7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -292,13 +292,28 @@ jobs:
           python3 tests/infra/platform_detection.py snp milan
         shell: bash
 
+      - name: "Build Lean recovery trace validator"
+        run: |
+          set -euo pipefail
+          curl --proto '=https' --tlsv1.2 -sSf \
+            https://raw.githubusercontent.com/leanprover/elan/58e8d545e33641f66dbcbd22c4283109e71757be/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          rm /tmp/elan-init.sh
+          export PATH="${HOME}/.elan/bin:${PATH}"
+          elan toolchain install "$(cat lean/disaster-recovery-trace/lean-toolchain)"
+          cd lean/disaster-recovery-trace
+          lake exe cache get
+          lake build trace-validator
+        shell: bash
+
       - name: "Build Debug"
         run: |
           set -ex
           git config --global --add safe.directory /__w/CCF/CCF
           mkdir build
           cd build
-          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 ..
+          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 -DCCF_RECOVERY_TRACE=ON ..
           ninja
         shell: bash
 
@@ -314,6 +329,7 @@ jobs:
         shell: bash
         env:
           CCF_TEST_SYNC_AFTER_SETUP: 1
+          CCF_LEAN_TRACE_VALIDATOR: ${{ github.workspace }}/lean/disaster-recovery-trace/.lake/build/bin/trace-validator
           ELECTION_TIMEOUT_MS: 10000
 
       - name: "Capture dmesg"
@@ -378,13 +394,28 @@ jobs:
           python3 tests/infra/platform_detection.py snp genoa
         shell: bash
 
+      - name: "Build Lean recovery trace validator"
+        run: |
+          set -euo pipefail
+          curl --proto '=https' --tlsv1.2 -sSf \
+            https://raw.githubusercontent.com/leanprover/elan/58e8d545e33641f66dbcbd22c4283109e71757be/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          rm /tmp/elan-init.sh
+          export PATH="${HOME}/.elan/bin:${PATH}"
+          elan toolchain install "$(cat lean/disaster-recovery-trace/lean-toolchain)"
+          cd lean/disaster-recovery-trace
+          lake exe cache get
+          lake build trace-validator
+        shell: bash
+
       - name: "Build Debug"
         run: |
           set -ex
           git config --global --add safe.directory /__w/CCF/CCF
           mkdir build
           cd build
-          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 ..
+          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 -DCCF_RECOVERY_TRACE=ON ..
           ninja
         shell: bash
 
@@ -400,6 +431,7 @@ jobs:
         shell: bash
         env:
           CCF_TEST_SYNC_AFTER_SETUP: 1
+          CCF_LEAN_TRACE_VALIDATOR: ${{ github.workspace }}/lean/disaster-recovery-trace/.lake/build/bin/trace-validator
           ELECTION_TIMEOUT_MS: 10000
 
       - name: "Capture dmesg"
diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
index d34e5678487..388ef79fef2 100644
--- a/.github/workflows/lean.yml
+++ b/.github/workflows/lean.yml
@@ -4,6 +4,14 @@ on:
   pull_request:
     paths:
       - "lean/**"
+      - "include/ccf/service/tables/self_healing_open.h"
+      - "src/node/recovery_decision_protocol.cpp"
+      - "src/node/recovery_decision_protocol.h"
+      - "src/node/rpc/self_healing_open_handlers.h"
+      - "tests/e2e_operations.py"
+      - "tests/infra/recovery_trace.py"
+      - "CMakeLists.txt"
+      - ".github/workflows/ci.yml"
       - ".github/workflows/lean.yml"
 
 concurrency:
@@ -45,3 +53,36 @@ jobs:
           lake build --wfail
           lake lint
           lake exe canonical-checks
+
+  trace-validator:
+    name: Trace validator
+    runs-on: ubuntu-26.04
+    timeout-minutes: 20
+
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install Lean
+        shell: bash
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y elan
+          elan toolchain install "$(cat lean/disaster-recovery-trace/lean-toolchain)"
+
+      - name: Restore Mathlib cache
+        working-directory: lean/disaster-recovery-trace
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
+      - name: Build and test validator
+        working-directory: lean/disaster-recovery-trace
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake exe mk_all --check --lib DisasterRecoveryTrace
+          lake build --wfail
+          lake lint
+          lake exe trace-checks
diff --git a/lean/disaster-recovery-trace/DisasterRecoveryTrace.lean b/lean/disaster-recovery-trace/DisasterRecoveryTrace.lean
new file mode 100644
index 00000000000..0ac2a8af41d
--- /dev/null
+++ b/lean/disaster-recovery-trace/DisasterRecoveryTrace.lean
@@ -0,0 +1,4 @@
+import DisasterRecoveryTrace.Protocol.Trace
+import DisasterRecoveryTrace.Protocol.Trace.Format
+import DisasterRecoveryTrace.Protocol.Trace.Logs
+import DisasterRecoveryTrace.Protocol.Trace.Replay
diff --git a/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace.lean b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace.lean
new file mode 100644
index 00000000000..ed6543ea4b4
--- /dev/null
+++ b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace.lean
@@ -0,0 +1,3 @@
+import DisasterRecoveryTrace.Protocol.Trace.Format
+import DisasterRecoveryTrace.Protocol.Trace.Logs
+import DisasterRecoveryTrace.Protocol.Trace.Replay
diff --git a/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Format.lean b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Format.lean
new file mode 100644
index 00000000000..fea56d9fc11
--- /dev/null
+++ b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Format.lean
@@ -0,0 +1,134 @@
+import DisasterRecovery.Protocol.Model
+import Lean.Data.Json
+import Lean.Data.Json.FromToJson
+
+namespace DisasterRecoveryTrace.Protocol.Trace
+
+open DisasterRecovery.Protocol.Model
+
+open Lean
+
+inductive Kind where
+  | start
+  | gossipAccepted
+  | voteAccepted
+  | iAmOpenAccepted
+  | timeout
+  | send
+  | open
+  | joinRestart
+  | complete
+deriving Repr, BEq, Inhabited
+
+structure TraceEvent where
+  instanceId : String
+  expectedLocations : List Location
+  node : Location
+  sequence : Nat
+  kind : Kind
+  messageId : Option String
+  causedBy : Option String
+  source : Option Location
+  txid : Option TxID
+  pre : Option Phase
+  post : Option Phase
+  openKind : Option OpenKind
+  send : Option String
+deriving Repr, BEq, Inhabited
+
+private def parseKind : String -> Except String Kind
+  | "start" => pure .start
+  | "gossip_accepted" => pure .gossipAccepted
+  | "vote_accepted" => pure .voteAccepted
+  | "iamopen_accepted" => pure .iAmOpenAccepted
+  | "timeout" => pure .timeout
+  | "send" => pure .send
+  | "open" => pure .open
+  | "join_restart" => pure .joinRestart
+  | "complete" => pure .complete
+  | value => throw s!"unknown kind '{value}'"
+
+private def parsePhase : String -> Except String Phase
+  | "GOSSIPING" => pure .gossiping
+  | "VOTING" => pure .voting
+  | "OPENING" => pure .opening
+  | "JOINING" => pure .joining
+  | "OPEN" => pure .open
+  | value => throw s!"unknown phase '{value}'"
+
+private def parseOpenKind : String -> Except String OpenKind
+  | "QUORUM" => pure .quorum
+  | "FAILOVER" => pure .failover
+  | value => throw s!"unknown open kind '{value}'"
+
+private def optionalString (json : Json) (key : String) :
+    Except String (Option String) :=
+  match json.getObjVal? key with
+  | .error _ | .ok .null => pure none
+  | .ok value => some <$> value.getStr?
+
+private def optionalNat (json : Json) (key : String) :
+    Except String (Option Nat) :=
+  match json.getObjVal? key with
+  | .error _ | .ok .null => pure none
+  | .ok value => some <$> value.getNat?
+
+private def optionalParsed
+    (json : Json)
+    (key : String)
+    (parse : String -> Except String α) :
+    Except String (Option α) := do
+  match <- optionalString json key with
+  | none => pure none
+  | some value => some <$> parse value
+
+def parseEvent (line : String) : Except String TraceEvent := do
+  let json <- Json.parse line
+  let view <- optionalNat json "view"
+  let seqno <- optionalNat json "seqno"
+  if view.isSome != seqno.isSome then
+    throw "view and seqno must appear together"
+
+  let instanceId <- json.getObjValAs? String "instance"
+  let expectedLocations <-
+    json.getObjValAs? (List String) "expected_locations"
+  let node <- json.getObjValAs? String "node"
+  let sequence <- json.getObjValAs? Nat "sequence"
+  let kindName <- json.getObjValAs? String "kind"
+  let kind <- parseKind kindName
+  let messageId <- optionalString json "message_id"
+  let causedBy <- optionalString json "caused_by"
+  let source <- optionalString json "source"
+  let pre <- optionalParsed json "pre" parsePhase
+  let post <- optionalParsed json "post" parsePhase
+  let openKind <- optionalParsed json "open_kind" parseOpenKind
+  let send <- optionalString json "send"
+  pure {
+    instanceId
+    expectedLocations
+    node
+    sequence
+    kind
+    messageId
+    causedBy
+    source
+    txid := match view, seqno with
+      | some view, some seqno => some { view, seqno }
+      | _, _ => none
+    pre
+    post
+    openKind
+    send
+  }
+
+def parseNDJSON (input : String) : Except String (List TraceEvent) := do
+  let lines := (input.splitOn "\n").filter
+    (fun line => !line.trimAscii.isEmpty)
+  let mut events := []
+  for (line, index) in lines.zipIdx do
+    match parseEvent line with
+    | .ok event => events := event :: events
+    | .error message => throw s!"line {index + 1}: {message}"
+  pure events.reverse
+
+end DisasterRecoveryTrace.Protocol.Trace
diff --git a/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Logs.lean b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Logs.lean
new file mode 100644
index 00000000000..4ce91f54b1e
--- /dev/null
+++ b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Logs.lean
@@ -0,0 +1,167 @@
+import DisasterRecoveryTrace.Protocol.Trace.Replay
+
+namespace DisasterRecoveryTrace.Protocol.Trace
+
+open DisasterRecovery.Protocol.Model
+open Lean
+
+inductive LogError where
+  | invalid (message : String)
+  | incomplete (message : String)
+deriving Repr, BEq
+
+structure LocatedEvent where
+  path : String
+  line : Nat
+  event : TraceEvent
+deriving Repr, BEq
+
+def LocatedEvent.origin (record : LocatedEvent) : String :=
+  s!"{record.path}:{record.line}"
+
+structure LogSnapshot where
+  events : List LocatedEvent := []
+  partialLines : List String := []
+deriving Repr
+
+private def logEvent (line : String) : Except String (Option TraceEvent) := do
+  let message <- match Json.parse line with
+    | .ok json =>
+        match json.getObjVal? "msg" with
+        | .ok (.str message) => pure message
+        | _ => pure ""
+    | .error _ => pure line
+  match message.splitOn "RDP_TRACE " with
+  | [] | [_] => pure none
+  | _ :: rest => some <$> parseEvent (String.intercalate "RDP_TRACE " rest)
+
+def extractLog (path input : String) : Except LogError LogSnapshot := do
+  let lines := input.splitOn "\n"
+  let mut snapshot : LogSnapshot := {}
+  -- Only newline-terminated records are stable while the node is writing.
+  for (line, index) in lines.dropLast.zipIdx do
+    match logEvent line with
+    | .error message =>
+        throw (.invalid s!"{path}:{index + 1}: invalid trace record: {message}")
+    | .ok none => pure ()
+    | .ok (some event) =>
+        snapshot := { snapshot with
+          events := { path, line := index + 1, event } :: snapshot.events }
+  if !(lines.getLast?.getD "").isEmpty then
+    snapshot := { snapshot with partialLines := [s!"{path}:{lines.length}"] }
+  pure { snapshot with events := snapshot.events.reverse }
+
+def extractLogBytes (path : String) (input : ByteArray) : Except LogError LogSnapshot := do
+  let mut endOffset := 0
+  let mut line := 1
+  for index in [:input.size] do
+    if input[index]! == 10 then
+      endOffset := index + 1
+      line := line + 1
+  let some text := String.fromUTF8? (input.extract 0 endOffset)
+    | throw (.invalid s!"{path}: invalid UTF-8 in newline-terminated log data")
+  let snapshot <- extractLog path text
+  pure { snapshot with
+    partialLines := if endOffset < input.size then [s!"{path}:{line}"] else [] }
+
+private def eventLE (a b : LocatedEvent) : Bool :=
+  a.event.node < b.event.node ||
+    (a.event.node == b.event.node && a.event.sequence <= b.event.sequence)
+
+def linearize (events : List LocatedEvent) :
+    Except LogError (List LocatedEvent) := do
+  let some first := events.head?
+    | throw (.incomplete "no recovery-decision-protocol trace events found")
+  let sorted := events.mergeSort eventLE
+  let mut previous : Option TraceEvent := none
+  let mut messageIds : List (String × LocatedEvent) := []
+  let mut missing : List String := []
+  for record in sorted do
+    let event := record.event
+    if event.instanceId != first.event.instanceId ||
+        event.expectedLocations != first.event.expectedLocations then
+      throw (.invalid s!"{record.origin}: recovery identity changed")
+    if let some id := event.messageId then
+      if messageIds.any (fun entry => entry.1 == id) then
+        throw (.invalid s!"{record.origin}: duplicate message_id '{id}'")
+      messageIds := (id, record) :: messageIds
+    let expected := match previous with
+      | some prev =>
+          if prev.node == event.node then prev.sequence + 1 else 0
+      | none => 0
+    if event.sequence < expected then
+      throw (.invalid s!"{record.origin}: duplicate node sequence {event.sequence}")
+    if event.sequence > expected then
+      missing := s!"{record.origin}: node {event.node} sequence {event.sequence}, expected {expected}"
+        :: missing
+    previous := some event
+  for record in sorted do
+    if let some cause := record.event.causedBy then
+      match messageIds.find? (fun entry => entry.1 == cause) with
+      | none =>
+          missing := s!"{record.origin}: caused_by '{cause}' has no matching send" :: missing
+      | some (_, source) =>
+          if source.event.kind != .send then
+            throw (.invalid s!"{record.origin}: caused_by '{cause}' does not identify a send")
+  if !missing.isEmpty then
+    throw (.incomplete (String.intercalate "\n" missing.reverse))
+
+  let mut remaining := sorted
+  let mut ordered : List LocatedEvent := []
+  let mut emittedIds : List String := []
+  let mut nextSequence : List (Location × Nat) := []
+  for _ in events do
+    let ready := remaining.find? fun record =>
+      let event := record.event
+      let sequence := (nextSequence.find? (fun entry => entry.1 == event.node)).map Prod.snd
+        |>.getD 0
+      event.sequence == sequence &&
+        (event.causedBy.map emittedIds.contains |>.getD true)
+    let some record := ready
+      | throw (.invalid "recovery trace contains a causal cycle")
+    remaining := remaining.filter fun other =>
+      other.event.node != record.event.node || other.event.sequence != record.event.sequence
+    ordered := record :: ordered
+    emittedIds := record.event.messageId.toList ++ emittedIds
+    nextSequence := (record.event.node, record.event.sequence + 1) ::
+      nextSequence.filter (fun entry => entry.1 != record.event.node)
+  pure ordered.reverse
+
+structure Scenario where
+  participatingNodes : Nat
+  openKind : OpenKind
+deriving Repr
+
+def validateLogs (logs : List (String × ByteArray)) (scenario : Scenario) :
+    Except LogError Nat := do
+  if scenario.participatingNodes == 0 then
+    throw (.invalid "expected participating-node count must be positive")
+  let mut events := []
+  let mut partialLines := []
+  for (path, input) in logs do
+    let snapshot <- extractLogBytes path input
+    events := events ++ snapshot.events
+    partialLines := partialLines ++ snapshot.partialLines
+  for record in events do
+    if record.event.kind == .open && record.event.openKind != some scenario.openKind then
+      throw (.invalid s!"{record.origin}: unexpected scenario open kind")
+  let ordered <- linearize events
+  let state <- match replay (ordered.map LocatedEvent.event) with
+    | .ok state => pure state
+    | .error failure =>
+        let origin := (ordered[failure.prefixLength - 1]?).map LocatedEvent.origin
+          |>.getD "trace"
+        throw (.invalid s!"{origin}: {renderFailure failure}")
+  let started := state.active.map (fun active => active.startedNodes.length) |>.getD 0
+  if started > scenario.participatingNodes then
+    throw (.invalid s!"started {started} nodes, expected {scenario.participatingNodes}")
+  if started < scenario.participatingNodes then
+    throw (.incomplete s!"started {started} nodes, expected {scenario.participatingNodes}")
+  match finish state ordered.length with
+  | .error failure => throw (.incomplete (renderFailure failure))
+  | .ok () => pure ()
+  if !partialLines.isEmpty then
+    throw (.incomplete s!"unterminated log lines: {String.intercalate ", " partialLines}")
+  pure ordered.length
+
+end DisasterRecoveryTrace.Protocol.Trace
diff --git a/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Replay.lean b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Replay.lean
new file mode 100644
index 00000000000..b9c6e7e11e9
--- /dev/null
+++ b/lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Replay.lean
@@ -0,0 +1,460 @@
+import DisasterRecoveryTrace.Protocol.Trace.Format
+
+namespace DisasterRecoveryTrace.Protocol.Trace
+
+open DisasterRecovery.Protocol.Model
+
+structure Failure where
+  prefixLength : Nat
+  message : String
+  expected : List String
+deriving Repr, BEq
+
+structure ObservedSend where
+  messageId : String
+  source : Location
+  description : String
+  txid : Option TxID
+deriving Repr, BEq
+
+structure PendingEffect where
+  node : Location
+  effect : Effect
+deriving Repr, BEq
+
+structure PendingSendBatch where
+  node : Location
+  remaining : List String
+deriving Repr, BEq
+
+structure ActiveReplay where
+  config : Config
+  system : SystemState
+  startedNodes : List Location
+  sends : List ObservedSend := []
+  consumedSendIds : List String := []
+  pendingEffects : List PendingEffect := []
+  pendingSendBatches : List PendingSendBatch := []
+  terminalNodes : List Location := []
+  completedNodes : List Location := []
+deriving Repr, BEq
+
+structure ReplayState where
+  active : Option ActiveReplay := none
+  nextSequence : List (Prod Location Nat) := []
+  seenMessageIds : List String := []
+deriving Repr, BEq, Inhabited
+
+private def nodeState (system : SystemState) (node : Location) : Option NodeState :=
+  (system.nodes.find? fun entry => entry.1 == node).map Prod.snd
+
+private def phaseMatches (expected : Option Phase) (actual : Phase) : Bool :=
+  expected == some actual
+
+private def isReceive : Kind -> Bool
+  | .gossipAccepted | .voteAccepted | .iAmOpenAccepted => true
+  | _ => false
+
+private def shapeError (event : TraceEvent) : Option String :=
+  if event.pre.isNone || event.post.isNone then
+    some "pre and post are required"
+  else if isReceive event.kind &&
+      (event.messageId.isNone || event.causedBy.isNone || event.source.isNone) then
+    some "message_id, caused_by, and source are required for receives"
+  else if event.kind == .gossipAccepted && event.txid.isNone then
+    some "view and seqno are required for gossip"
+  else if event.kind == .send &&
+      (event.messageId.isNone || event.send.isNone) then
+    some "message_id and send are required for sends"
+  else if event.kind == .send &&
+      (event.send.getD "").startsWith "gossip:" && event.txid.isNone then
+    some "view and seqno are required for gossip sends"
+  else if event.kind == .open && event.openKind.isNone then
+    some "open_kind is required for open"
+  else if !isReceive event.kind && event.causedBy.isSome then
+    some "caused_by is only valid on receive events"
+  else if event.messageId.map String.isEmpty |>.getD false then
+    some "message_id must not be empty"
+  else if event.causedBy.map String.isEmpty |>.getD false then
+    some "caused_by must not be empty"
+  else if event.source.map String.isEmpty |>.getD false then
+    some "source must not be empty"
+  else
+    none
+
+private def configError (config : Config) : Option String :=
+  if config.instanceId.isEmpty then
+    some "instance must not be empty"
+  else if config.expectedLocations.isEmpty then
+    some "expected_locations must not be empty"
+  else if config.expectedLocations.any String.isEmpty then
+    some "expected_locations must not contain an empty name"
+  else if config.expectedLocations.eraseDups.length !=
+      config.expectedLocations.length then
+    some "expected_locations must not contain duplicates"
+  else
+    none
+
+private def expectedSequence (state : ReplayState) (node : Location) : Nat :=
+  (state.nextSequence.find? fun entry => entry.1 == node).map Prod.snd |>.getD 0
+
+private def setSequence
+    (sequences : List (Prod Location Nat))
+    (node : Location)
+    (next : Nat) :
+    List (Prod Location Nat) :=
+  if sequences.any (fun entry => entry.1 == node) then
+    sequences.map fun entry => if entry.1 == node then (node, next) else entry
+  else
+    (node, next) :: sequences
+
+private def effectName : Effect -> Option String
+  | .sendGossip destination => some s!"gossip:{destination}"
+  | .sendVote destination => some s!"vote:{destination}"
+  | .sendIAmOpen destination => some s!"iamopen:{destination}"
+  | _ => none
+
+private def sendBatch (config : Config) (state : NodeState) : List String :=
+  (step config state .retry).effects.filterMap effectName
+
+private def setPendingSendBatch
+    (node : Location)
+    (remaining : List String)
+    (batches : List PendingSendBatch) :
+    List PendingSendBatch :=
+  let others := batches.filter (fun batch => batch.node != node)
+  if remaining.isEmpty then
+    others
+  else
+    { node, remaining } :: others
+
+private def receiveDescription (event : TraceEvent) : Option String :=
+  match event.kind with
+  | .gossipAccepted => some s!"gossip:{event.node}"
+  | .voteAccepted => some s!"vote:{event.node}"
+  | .iAmOpenAccepted => some s!"iamopen:{event.node}"
+  | _ => none
+
+private def eventInput (event : TraceEvent) : Option Event :=
+  match event.kind, event.source, event.txid with
+  | .gossipAccepted, some source, some txid =>
+      some (.receiveGossip source txid .accepted)
+  | .voteAccepted, some source, _ =>
+      some (.receiveVote source .accepted)
+  | .iAmOpenAccepted, some source, _ =>
+      some (.receiveIAmOpen source .accepted)
+  | .timeout, _, _ => some .timeout
+  | _, _, _ => none
+
+private def isOneShotEffect : Effect -> Bool
+  | .opening _ | .restart _ | .completed => true
+  | _ => false
+
+private def addEffects
+    (node : Location)
+    (effects : List Effect)
+    (pending : List PendingEffect) :
+    List PendingEffect :=
+  pending ++ (effects.filter isOneShotEffect).map fun effect =>
+    ({ node := node, effect := effect } : PendingEffect)
+
+private def removeEffect (node : Location) (target : Effect) :
+    List PendingEffect -> Option (List PendingEffect)
+  | [] => none
+  | pending :: rest =>
+      if pending.node == node && pending.effect == target then
+        some rest
+      else
+        (removeEffect node target rest).map (fun remaining =>
+          pending :: remaining)
+
+private def removeRestart (node : Location) :
+    List PendingEffect -> Option (List PendingEffect)
+  | [] => none
+  | pending :: rest =>
+      if pending.node == node then
+        match pending.effect with
+        | .restart _ => some rest
+        | _ => (removeRestart node rest).map (fun remaining =>
+            pending :: remaining)
+      else
+        (removeRestart node rest).map (fun remaining => pending :: remaining)
+
+private def consumeCause
+    (active : ActiveReplay)
+    (event : TraceEvent) : Except String ActiveReplay := do
+  let cause := event.causedBy.getD ""
+  if active.consumedSendIds.contains cause then
+    throw s!"caused_by '{cause}' was already consumed"
+  let send <- match active.sends.find? (fun send => send.messageId == cause) with
+    | none => throw s!"caused_by '{cause}' has no prior send"
+    | some send => pure send
+  let source := event.source.getD ""
+  let description := receiveDescription event |>.getD ""
+  if send.source != source || send.description != description then
+    throw s!"caused_by '{cause}' has the wrong source, class, or destination"
+  if event.kind == .gossipAccepted && send.txid != event.txid then
+    throw s!"caused_by '{cause}' has the wrong gossip TxID"
+  pure {
+    active with
+    consumedSendIds := cause :: active.consumedSendIds
+  }
+
+private def applyTransition
+    (active : ActiveReplay)
+    (event : TraceEvent) : Except String ActiveReplay := do
+  let before <- match nodeState active.system event.node with
+    | none => throw s!"unknown node {event.node}"
+    | some state => pure state
+  if !phaseMatches event.pre before.phase then
+    throw s!"pre phase does not match {phaseName before.phase}"
+  let input <- match eventInput event with
+    | none => throw "event is not a protocol transition"
+    | some input => pure input
+  let (system, output) <- match
+      systemStep active.config active.system event.node input with
+    | none => throw s!"unknown node {event.node}"
+    | some result => pure result
+  if !output.accepted then
+    throw "protocol transition was rejected"
+  if !phaseMatches event.post output.state.phase then
+    throw s!"post phase does not match {phaseName output.state.phase}"
+  pure {
+    active with
+    system
+    pendingEffects :=
+      addEffects event.node output.effects active.pendingEffects
+  }
+
+private def applyReceive
+    (active : ActiveReplay)
+    (event : TraceEvent) : Except String ActiveReplay := do
+  applyTransition (← consumeCause active event) event
+
+private def applySend
+    (active : ActiveReplay)
+    (event : TraceEvent) : Except String ActiveReplay := do
+  let state <- match nodeState active.system event.node with
+    | none => throw s!"unknown node {event.node}"
+    | some state => pure state
+  if !phaseMatches event.pre state.phase || !phaseMatches event.post state.phase then
+    throw s!"send phase does not match {phaseName state.phase}"
+  let description := event.send.getD ""
+  let batch := (active.pendingSendBatches.find?
+    (fun batch => batch.node == event.node)).map (fun batch => batch.remaining)
+    |>.getD (sendBatch active.config state)
+  let expected <- match batch with
+    | [] => throw "no retry send batch is enabled"
+    | expected :: _ => pure expected
+  if description != expected then
+    throw s!"expected send '{expected}', got '{description}'"
+  pure {
+    active with
+    sends := {
+      messageId := event.messageId.getD ""
+      source := event.node
+      description
+      txid := event.txid
+    } :: active.sends
+    pendingSendBatches :=
+      setPendingSendBatch event.node batch.tail active.pendingSendBatches
+  }
+
+private def applyObservation
+    (active : ActiveReplay)
+    (event : TraceEvent) : Except String ActiveReplay := do
+  let state <- match nodeState active.system event.node with
+    | none => throw s!"unknown node {event.node}"
+    | some state => pure state
+  if !phaseMatches event.pre state.phase || !phaseMatches event.post state.phase then
+    throw s!"observation phase does not match {phaseName state.phase}"
+  match event.kind with
+    | .open =>
+        if state.phase != .opening || event.openKind != state.openKind then
+          throw "open observation does not match state"
+        let pendingEffects <- match
+            removeEffect event.node (.opening event.openKind.get!) active.pendingEffects with
+        | none => throw "open observation has no pending opening effect"
+        | some pending => pure pending
+        pure { active with pendingEffects }
+    | .joinRestart =>
+        if state.phase != .joining || !state.restartRequested then
+          throw "join_restart observation does not match state"
+        let pendingEffects <- match removeRestart event.node active.pendingEffects with
+        | none => throw "join_restart has no pending restart effect"
+        | some pending => pure pending
+        pure {
+          active with
+          pendingEffects
+          terminalNodes := event.node :: active.terminalNodes
+        }
+    | .complete =>
+        if state.phase != .open then
+          throw "complete observation does not match state"
+        let pendingEffects <- match
+            removeEffect event.node .completed active.pendingEffects with
+        | none => throw "complete has no pending completion effect"
+        | some pending => pure pending
+        pure {
+          active with
+          pendingEffects
+          terminalNodes := event.node :: active.terminalNodes
+          completedNodes := event.node :: active.completedNodes
+        }
+    | _ => throw "event is not a protocol observation"
+
+private def expectedEvents (active : ActiveReplay) (node : Location) :
+    List String :=
+  let phase := nodeState active.system node |>.map
+    (fun state => phaseName state.phase) |>.getD "UNKNOWN"
+  [s!"state={phase}", "send", "gossip_accepted", "vote_accepted",
+    "iamopen_accepted", "timeout", "open", "join_restart", "complete"]
+
+private def start
+    (active : Option ActiveReplay)
+    (config : Config)
+    (event : TraceEvent) : Except String ActiveReplay := do
+  if !config.expectedLocations.contains event.node then
+    throw s!"start node {event.node} is not expected"
+  let current := active.getD {
+    config
+    system := initialSystem config
+    startedNodes := []
+  }
+  if current.config != config then
+    throw "instance or expected_locations changed"
+  if current.startedNodes.contains event.node then
+    throw s!"duplicate start event for node {event.node}"
+  let state <- match nodeState current.system event.node with
+    | none => throw s!"unknown node {event.node}"
+    | some state => pure state
+  if !phaseMatches event.pre state.phase || !phaseMatches event.post state.phase then
+    throw "start pre/post phase does not match GOSSIPING"
+  pure {
+    current with
+    startedNodes := event.node :: current.startedNodes
+  }
+
+private def processActive
+    (active : ActiveReplay)
+    (event : TraceEvent) : Except String ActiveReplay := do
+  if active.config.instanceId != event.instanceId ||
+      active.config.expectedLocations != event.expectedLocations then
+    throw "instance or expected_locations changed"
+  if !active.startedNodes.contains event.node then
+    throw s!"node {event.node} has no start event"
+  if event.kind != .send &&
+      active.pendingSendBatches.any (fun batch => batch.node == event.node) then
+    throw s!"node {event.node} has an incomplete retry send batch"
+  match event.kind with
+  | .gossipAccepted | .voteAccepted | .iAmOpenAccepted =>
+      applyReceive active event
+  | .timeout => applyTransition active event
+  | .send => applySend active event
+  | .open | .joinRestart | .complete => applyObservation active event
+  | .start => throw "unexpected start event"
+
+private def fail
+    (index : Nat)
+    (message : String)
+    (expected : List String := []) :
+    Except Failure α :=
+  throw { prefixLength := index + 1, message, expected }
+
+private def process
+    (index : Nat)
+    (state : ReplayState)
+    (event : TraceEvent) : Except Failure ReplayState := do
+  if let some message := shapeError event then
+    fail index message
+  let config : Config := {
+    instanceId := event.instanceId
+    expectedLocations := event.expectedLocations
+  }
+  if let some message := configError config then
+    fail index message
+  let expectedSeq := expectedSequence state event.node
+  if event.sequence != expectedSeq then
+    fail index s!"node {event.node} sequence {event.sequence}, expected {expectedSeq}"
+  if let some messageId := event.messageId then
+    if state.seenMessageIds.contains messageId then
+      fail index s!"message_id '{messageId}' was already used"
+    if event.causedBy == some messageId then
+      fail index "message_id and caused_by must identify distinct observations"
+
+  let nextActive <- match event.kind with
+    | .start =>
+        match start state.active config event with
+        | .ok active => pure active
+        | .error message => fail index message
+    | _ =>
+        match state.active with
+        | none => fail index "trace must begin with start" ["start"]
+        | some active =>
+            match processActive active event with
+            | .ok next => pure next
+            | .error message => fail index message (expectedEvents active event.node)
+
+  pure {
+    active := some nextActive
+    nextSequence :=
+      setSequence state.nextSequence event.node (expectedSeq + 1)
+    seenMessageIds := event.messageId.toList ++ state.seenMessageIds
+  }
+
+def replay (events : List TraceEvent) : Except Failure ReplayState := do
+  if events.isEmpty then
+    throw {
+      prefixLength := 0
+      message := "empty trace"
+      expected := ["start"]
+    }
+  let mut state : ReplayState := {}
+  for (event, index) in events.zipIdx do
+    state <- process index state event
+  pure state
+
+def finish (state : ReplayState) (eventCount : Nat) : Except Failure Unit := do
+  let active <- match state.active with
+    | none =>
+        throw {
+          prefixLength := eventCount
+          message := "trace has no start event"
+          expected := ["start"]
+        }
+    | some active => pure active
+  if !active.pendingEffects.isEmpty then
+    throw {
+      prefixLength := eventCount
+      message := "trace ended with unobserved committed effects"
+      expected := ["open", "join_restart", "complete"]
+    }
+  if !active.pendingSendBatches.isEmpty then
+    throw {
+      prefixLength := eventCount
+      message := "trace ended with incomplete retry send batches"
+      expected := ["send"]
+    }
+  if !active.startedNodes.all (fun node => active.terminalNodes.contains node) then
+    throw {
+      prefixLength := eventCount
+      message := "trace ended before every participating node terminated"
+      expected := ["join_restart", "complete"]
+    }
+  if active.completedNodes.isEmpty then
+    throw {
+      prefixLength := eventCount
+      message := "trace has no completed opener"
+      expected := ["complete"]
+    }
+
+def validate (events : List TraceEvent) : Except Failure Unit := do
+  finish (← replay events) events.length
+
+def renderFailure (failure : Failure) : String :=
+  let expected :=
+    if failure.expected.isEmpty then ""
+    else s!"\nexpected compatible events:\n  {String.intercalate "\n  " failure.expected}"
+  s!"shortest failing prefix: {failure.prefixLength}\n{failure.message}{expected}"
+
+end DisasterRecoveryTrace.Protocol.Trace
diff --git a/lean/disaster-recovery-trace/README.md b/lean/disaster-recovery-trace/README.md
new file mode 100644
index 00000000000..5efccf19958
--- /dev/null
+++ b/lean/disaster-recovery-trace/README.md
@@ -0,0 +1,51 @@
+# Disaster recovery trace validation
+
+This package validates implementation traces from CCF's C++ recovery
+decision protocol against the permanent model in `../disaster-recovery`. It is
+deliberately separate from the canonical model and depends only on
+`DisasterRecovery.Protocol.Model`. Both packages are pinned to Lean 4.33.1.
+
+`DisasterRecoveryTrace.Protocol.Trace.Format` parses the strict
+NDJSON contract. `DisasterRecoveryTrace.Protocol.Trace.Logs` extracts records
+directly from text or JSON node logs and orders them using per-node sequences
+and causal send edges, not timestamps.
+`DisasterRecoveryTrace.Protocol.Trace.Replay` replays each event against the
+canonical transition system. The validator rejects the first incompatible event
+and reports its original file/line location and shortest failing ordered prefix.
+
+## Build and test
+
+```sh
+lake exe cache get
+lake exe mk_all --check --lib DisasterRecoveryTrace
+lake build --wfail
+lake lint
+lake exe trace-checks
+```
+
+Run the validator with:
+
+```sh
+lake exe trace-validator --logs 3 QUORUM 20000 node0/out node1/out node2/out
+```
+
+The arguments are the expected participating-node count, expected open kind
+(`QUORUM` or `FAILOVER`), timeout in milliseconds, and raw log paths. Lean waits
+for complete newline-terminated records and scenario terminal evidence. Missing
+sequences, send causes, or terminal effects are incomplete input; if they do not
+arrive before the deadline, validation fails. Malformed records, causal cycles,
+duplicate identifiers, wrong outcomes, and invalid replay transitions fail
+without retrying. File read errors also fail rather than silently skipping logs.
+Python only supplies log paths and scenario expectations and reports the result.
+
+The original node logs are the reproduction artifact uploaded by SNP CI. For
+an offline check use a timeout of `0`. Already ordered NDJSON remains supported
+with `lake exe trace-validator TRACE.ndjson`; it does not perform the additional
+scenario checks.
+
+`TraceTests.lean` contains parser, ordering, scenario, and replay tests. These tests
+exercise rejection behavior; they are not implementation conformance evidence.
+Conformance evidence is produced only from real C++ SNP recovery runs and is
+uploaded by the Milan and Genoa jobs.
+
+See [TRACE_FORMAT.md](TRACE_FORMAT.md) for the complete contract.
diff --git a/lean/disaster-recovery-trace/TraceMain.lean b/lean/disaster-recovery-trace/TraceMain.lean
new file mode 100644
index 00000000000..4a5e81780fe
--- /dev/null
+++ b/lean/disaster-recovery-trace/TraceMain.lean
@@ -0,0 +1,55 @@
+import DisasterRecoveryTrace.Protocol.Trace
+
+open DisasterRecoveryTrace.Protocol.Trace
+
+private def validateLogFiles
+    (paths : List String) (scenario : Scenario) (timeoutMs : Nat) : IO UInt32 := do
+  let deadline := (← IO.monoMsNow) + timeoutMs
+  repeat
+    let logs <- paths.mapM fun (path : String) => do
+      pure (path, ← IO.FS.readBinFile path)
+    match validateLogs logs scenario with
+    | .ok count =>
+        IO.println s!"trace accepted: {count} events from {paths.length} logs"
+        return 0
+    | .error (.invalid message) =>
+        IO.eprintln message
+        return 1
+    | .error (.incomplete message) =>
+        if (← IO.monoMsNow) >= deadline then
+          IO.eprintln s!"timed out waiting for a complete recovery trace:\n{message}"
+          return 1
+        IO.sleep 100
+
+private def usage : IO UInt32 := do
+  IO.eprintln ("usage: trace-validator TRACE.ndjson\n" ++
+    "       trace-validator --logs NODE_COUNT QUORUM|FAILOVER TIMEOUT_MS LOG...")
+  pure 2
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | "--logs" :: count :: kind :: timeout :: paths => do
+      let some participatingNodes := count.toNat? | usage
+      let some timeoutMs := timeout.toNat? | usage
+      let openKind <- match kind with
+        | "QUORUM" => pure DisasterRecovery.Protocol.Model.OpenKind.quorum
+        | "FAILOVER" => pure DisasterRecovery.Protocol.Model.OpenKind.failover
+        | _ => return ← usage
+      if participatingNodes == 0 || paths.isEmpty then
+        return ← usage
+      validateLogFiles paths { participatingNodes, openKind } timeoutMs
+  | [path] =>
+      let input <- IO.FS.readFile path
+      match parseNDJSON input with
+      | .error message =>
+          IO.eprintln message
+          pure 1
+      | .ok events =>
+          match validate events with
+          | .error failure =>
+              IO.eprintln (renderFailure failure)
+              pure 1
+          | .ok () =>
+              IO.println s!"trace accepted: {events.length} events"
+              pure 0
+  | _ => usage
diff --git a/lean/disaster-recovery-trace/TraceTests.lean b/lean/disaster-recovery-trace/TraceTests.lean
new file mode 100644
index 00000000000..8a0361a8695
--- /dev/null
+++ b/lean/disaster-recovery-trace/TraceTests.lean
@@ -0,0 +1,495 @@
+import DisasterRecoveryTrace.Protocol.Trace
+
+open DisasterRecovery.Protocol.Model
+open DisasterRecoveryTrace.Protocol.Trace
+
+private def expect (condition : Bool) (message : String) : IO Unit :=
+  unless condition do throw (IO.userError message)
+
+private def baseEvent
+    (locations : List Location)
+    (node : Location)
+    (sequence : Nat)
+    (kind : Kind) : TraceEvent := {
+  instanceId := "trace-tests"
+  expectedLocations := locations
+  node
+  sequence
+  kind
+  messageId := none
+  causedBy := none
+  source := none
+  txid := none
+  pre := none
+  post := none
+  openKind := none
+  send := none
+}
+
+private def startEvent
+    (locations : List Location)
+    (node : Location) : TraceEvent := {
+  baseEvent locations node 0 .start with
+  pre := some .gossiping
+  post := some .gossiping
+}
+
+private def sendEvent
+    (locations : List Location)
+    (sequence : Nat)
+    (messageId description : String)
+    (phase : Phase) : TraceEvent := {
+  baseEvent locations "A" sequence .send with
+  messageId := some messageId
+  pre := some phase
+  post := some phase
+  txid := if description.startsWith "gossip:" then
+    some { view := 1, seqno := 1 }
+  else
+    none
+  send := some description
+}
+
+private def gossipEvent
+    (locations : List Location)
+    (sequence : Nat)
+    (messageId cause : String)
+    (post : Phase) : TraceEvent := {
+  baseEvent locations "A" sequence .gossipAccepted with
+  messageId := some messageId
+  causedBy := some cause
+  source := some "A"
+  txid := some { view := 1, seqno := 1 }
+  pre := some .gossiping
+  post := some post
+}
+
+private def voteEvent
+    (locations : List Location)
+    (sequence : Nat)
+    (messageId cause : String)
+    (post : Phase) : TraceEvent := {
+  baseEvent locations "A" sequence .voteAccepted with
+  messageId := some messageId
+  causedBy := some cause
+  source := some "A"
+  pre := some .voting
+  post := some post
+}
+
+private def timeoutEvent
+    (locations : List Location)
+    (sequence : Nat)
+    (pre post : Phase) : TraceEvent := {
+  baseEvent locations "A" sequence .timeout with
+  pre := some pre
+  post := some post
+}
+
+private def openEvent
+    (locations : List Location)
+    (sequence : Nat)
+    (kind : OpenKind) : TraceEvent := {
+  baseEvent locations "A" sequence .open with
+  pre := some .opening
+  post := some .opening
+  openKind := some kind
+}
+
+private def completeEvent
+    (locations : List Location)
+    (sequence : Nat) : TraceEvent := {
+  baseEvent locations "A" sequence .complete with
+  pre := some .open
+  post := some .open
+}
+
+private def validationSucceeds (events : List TraceEvent) : Bool :=
+  match validate events with
+  | .ok () => true
+  | .error _ => false
+
+private def failedAt (events : List TraceEvent) (expectedPrefix : Nat) : Bool :=
+  match validate events with
+  | .error failure => failure.prefixLength == expectedPrefix
+  | .ok () => false
+
+private def parseFails (value : String) : Bool :=
+  match parseEvent value with
+  | .error _ => true
+  | .ok _ => false
+
+private def quorumTrace : List TraceEvent :=
+  let locations := ["A"]
+  [
+    startEvent locations "A",
+    sendEvent locations 1 "send-gossip" "gossip:A" .gossiping,
+    gossipEvent locations 2 "receive-gossip" "send-gossip" .voting,
+    sendEvent locations 3 "send-vote" "vote:A" .voting,
+    sendEvent locations 4 "send-voting-gossip" "gossip:A" .voting,
+    voteEvent locations 5 "receive-vote" "send-vote" .opening,
+    openEvent locations 6 .quorum,
+    timeoutEvent locations 7 .opening .opening,
+    timeoutEvent locations 8 .opening .opening,
+    timeoutEvent locations 9 .opening .open,
+    completeEvent locations 10
+  ]
+
+private def eventJson (event : TraceEvent) : Lean.Json :=
+  let kind := match event.kind with
+    | .start => "start"
+    | .send => "send"
+    | .gossipAccepted => "gossip_accepted"
+    | .voteAccepted => "vote_accepted"
+    | .iAmOpenAccepted => "iamopen_accepted"
+    | .timeout => "timeout"
+    | .open => "open"
+    | .joinRestart => "join_restart"
+    | .complete => "complete"
+  Lean.Json.mkObj ([
+    ("instance", Lean.toJson event.instanceId),
+    ("expected_locations", Lean.toJson event.expectedLocations),
+    ("node", Lean.toJson event.node),
+    ("sequence", Lean.toJson event.sequence),
+    ("kind", Lean.toJson kind)
+  ] ++
+    (event.messageId.toList.map fun value => ("message_id", Lean.toJson value)) ++
+    (event.causedBy.toList.map fun value => ("caused_by", Lean.toJson value)) ++
+    (event.source.toList.map fun value => ("source", Lean.toJson value)) ++
+    (event.txid.toList.flatMap fun value =>
+      [("view", Lean.toJson value.view), ("seqno", Lean.toJson value.seqno)]) ++
+    (event.pre.toList.map fun value => ("pre", Lean.toJson (phaseName value))) ++
+    (event.post.toList.map fun value => ("post", Lean.toJson (phaseName value))) ++
+    (event.openKind.toList.map fun value => ("open_kind", Lean.toJson (openKindName value))) ++
+    (event.send.toList.map fun value => ("send", Lean.toJson value)))
+
+private def textLog (events : List TraceEvent) : String :=
+  String.join (events.map fun event => s!"[info] RDP_TRACE {(eventJson event).compress}\n")
+
+private def jsonLog (events : List TraceEvent) : String :=
+  String.join (events.map fun event =>
+    (Lean.Json.mkObj [("msg", Lean.toJson s!"RDP_TRACE {(eventJson event).compress}")]).compress
+      ++ "\n")
+
+private def located (events : List TraceEvent) : List LocatedEvent :=
+  events.zipIdx.map fun (event, index) => { path := "test.out", line := index + 1, event }
+
+private def expectInvalid (result : Except LogError α) (message : String) : IO Unit := do
+  match result with
+  | .error (.invalid _) => pure ()
+  | _ => throw (IO.userError message)
+
+private def expectIncomplete (result : Except LogError α) (message : String) : IO Unit := do
+  match result with
+  | .error (.incomplete _) => pure ()
+  | _ => throw (IO.userError message)
+
+private def accepted [BEq α] (result : Except LogError α) (expected : α) : Bool :=
+  match result with
+  | .ok value => value == expected
+  | .error _ => false
+
+private def validateTextLogs (logs : List (String × String)) (scenario : Scenario) :
+    Except LogError Nat :=
+  validateLogs (logs.map fun (path, text) => (path, text.toUTF8)) scenario
+
+private def checkLogs : IO Unit := do
+  let scenario : Scenario := { participatingNodes := 1, openKind := .quorum }
+  let logs := [("node.out", textLog quorumTrace)]
+  expect (accepted (validateTextLogs logs scenario) quorumTrace.length)
+    "raw text quorum log was rejected"
+  expect
+    (accepted
+      (validateTextLogs [("node.out", "unrelated\n{\"msg\":42}\n\n" ++ jsonLog quorumTrace)] scenario)
+      quorumTrace.length)
+    "JSON envelope quorum log was rejected"
+  expect
+    (accepted (validateTextLogs [("node.out", textLog quorumTrace.reverse)] scenario)
+      quorumTrace.length)
+    "per-node sequences were not used to order records"
+  expect
+    (accepted (validateTextLogs [("node.out", (textLog quorumTrace).replace "\n" "\r\n")] scenario)
+      quorumTrace.length)
+    "CRLF log was rejected"
+
+  let first := quorumTrace.head!
+  let escaped := quorumTrace.map fun event =>
+    { event with instanceId := "escaped \"quote\" \\ slash RDP_TRACE value" }
+  expect
+    (accepted (validateTextLogs [("node.out", jsonLog escaped)] scenario) escaped.length)
+    "escaped JSON message or embedded marker was misparsed"
+  expectInvalid (extractLog "bad.out" "noise\nRDP_TRACE {broken}\n")
+    "malformed marked record was ignored"
+  expectInvalid (extractLog "bad.out" s!"RDP_TRACE {(eventJson first).compress} junk\n")
+    "trailing garbage after an event was ignored"
+  match extractLog "bad.out" "noise\nRDP_TRACE {broken}\n" with
+  | .error (.invalid message) =>
+      expect (message.startsWith "bad.out:2:") "raw source location was lost"
+  | _ => throw (IO.userError "malformed input accepted")
+  expectIncomplete (validateTextLogs [] scenario) "empty trace was accepted"
+  expectIncomplete (validateTextLogs [("node.out", textLog (quorumTrace.take 6))] scenario)
+    "unobserved committed effect was accepted"
+  expectIncomplete (validateTextLogs [("node.out", textLog quorumTrace.dropLast)] scenario)
+    "missing completion was accepted"
+  expectIncomplete
+    (validateTextLogs [("node.out", textLog quorumTrace ++ "RDP_TRACE {")] scenario)
+    "unterminated record after completion was accepted"
+  expectIncomplete
+    (validateTextLogs logs { scenario with participatingNodes := 2 })
+    "absent participating node was accepted"
+  expectInvalid (validateTextLogs logs { scenario with participatingNodes := 0 })
+    "zero participating nodes was accepted"
+  expectInvalid (validateTextLogs logs { scenario with openKind := .failover })
+    "wrong scenario open kind was accepted"
+  expectInvalid
+    (validateTextLogs [("node.out", textLog (quorumTrace ++ [first]))] scenario)
+    "duplicate node sequence was accepted"
+  expectIncomplete
+    (linearize (located [first, { first with sequence := 2, kind := .timeout }]))
+    "sequence gap was accepted"
+  expectInvalid
+    (linearize (located [first, { first with sequence := 1, instanceId := "other" }]))
+    "recovery identity change was accepted"
+  expectInvalid
+    (linearize (located [
+      { first with messageId := some "duplicate" },
+      { first with sequence := 1, messageId := some "duplicate" }
+    ]))
+    "duplicate message ID was accepted"
+  expectIncomplete
+    (linearize (located [first, gossipEvent ["A"] 1 "receive" "missing" .voting]))
+    "unresolved cause was accepted"
+  expectInvalid
+    (linearize (located [
+      { first with messageId := some "not-a-send" },
+      gossipEvent ["A"] 1 "receive" "not-a-send" .voting
+    ]))
+    "receive used a non-send cause"
+  expectInvalid
+    (validateTextLogs [("node.out", textLog (quorumTrace.map fun event =>
+      if event.sequence == 2 then { event with post := some .open } else event))] scenario)
+    "invalid replay transition was treated as incomplete input"
+  let partialUTF8 := (textLog quorumTrace).toUTF8.push 0xc3
+  expectIncomplete (validateLogs [("node.out", partialUTF8)] scenario)
+    "partial UTF-8 write was accepted or treated as malformed"
+  expectInvalid (validateLogs [("node.out", partialUTF8.push 10)] scenario)
+    "malformed UTF-8 in a complete line was accepted"
+
+  let locations := ["A", "B"]
+  let aStart := startEvent locations "A"
+  let bStart := startEvent locations "B"
+  let aReceive := {
+    gossipEvent locations 1 "receive-a" "send-b" .gossiping with source := some "B" }
+  let bReceive := {
+    gossipEvent locations 1 "receive-b" "send-a" .gossiping with node := "B" }
+  let aSend := sendEvent locations 2 "send-a" "gossip:B" .gossiping
+  let bSend := { sendEvent locations 2 "send-b" "gossip:A" .gossiping with node := "B" }
+  expectInvalid (linearize (located [aStart, aReceive, aSend, bStart, bReceive, bSend]))
+    "causal cycle was accepted"
+  let causal := [aStart, aReceive, bStart, { bSend with sequence := 1 }]
+  match linearize (located causal) with
+  | .ok records =>
+      expect
+        (records.map (fun record => (record.event.node, record.event.sequence)) ==
+          [("A", 0), ("B", 0), ("B", 1), ("A", 1)])
+        "cross-node cause did not precede its receive"
+  | .error error => throw (IO.userError s!"causal trace rejected: {repr error}")
+  match linearize (located causal), linearize (located causal.reverse) with
+  | .ok forward, .ok backward =>
+      expect (forward.map LocatedEvent.event == backward.map LocatedEvent.event)
+        "ordering depends on log argument order"
+  | _, _ => throw (IO.userError "causal ordering failed")
+
+private def failoverTrace : List TraceEvent :=
+  let locations := ["A", "B"]
+  [
+    startEvent locations "A",
+    sendEvent locations 1 "gossip-a" "gossip:A" .gossiping,
+    sendEvent locations 2 "gossip-b" "gossip:B" .gossiping,
+    gossipEvent locations 3 "receive-gossip" "gossip-a" .gossiping,
+    timeoutEvent locations 4 .gossiping .voting,
+    sendEvent locations 5 "vote-a" "vote:A" .voting,
+    sendEvent locations 6 "voting-gossip-a" "gossip:A" .voting,
+    sendEvent locations 7 "voting-gossip-b" "gossip:B" .voting,
+    voteEvent locations 8 "receive-vote" "vote-a" .voting,
+    timeoutEvent locations 9 .voting .opening,
+    openEvent locations 10 .failover,
+    timeoutEvent locations 11 .opening .open,
+    completeEvent locations 12
+  ]
+
+private def checkMultiNodeLogs : IO Unit := do
+  let locations := ["A", "B"]
+  let opener := failoverTrace.take 11 ++ [
+    sendEvent locations 11 "send-open-b" "iamopen:B" .opening,
+    timeoutEvent locations 12 .opening .open,
+    completeEvent locations 13
+  ]
+  let joiner := [
+    startEvent locations "B",
+    { baseEvent locations "B" 1 .iAmOpenAccepted with
+      messageId := some "receive-open-b"
+      causedBy := some "send-open-b"
+      source := some "A"
+      pre := some .gossiping
+      post := some .joining },
+    { baseEvent locations "B" 2 .joinRestart with
+      pre := some .joining
+      post := some .joining }
+  ]
+  let logs := [("b.out", jsonLog joiner), ("a.out", textLog opener)]
+  let scenario : Scenario := { participatingNodes := 2, openKind := .failover }
+  expect (accepted (validateTextLogs logs scenario) (opener.length + joiner.length))
+    "distributed opener/joiner logs were rejected"
+  expect (accepted (validateTextLogs logs.reverse scenario) (opener.length + joiner.length))
+    "log path order changed distributed validation"
+  expectIncomplete
+    (validateTextLogs [("b.out", jsonLog joiner.dropLast), ("a.out", textLog opener)] scenario)
+    "unterminated joiner was accepted"
+  expectInvalid (validateTextLogs logs { scenario with participatingNodes := 1 })
+    "extra participating node was accepted"
+
+private def checkLogCLI : IO Unit := do
+  IO.FS.withTempDir fun directory => do
+    let path := directory / "node log.out"
+    let validator := ".lake/build/bin/trace-validator"
+    let run := fun (kind : String) (timeout : String) => IO.Process.output {
+      cmd := validator
+      args := #["--logs", "1", kind, timeout, path.toString]
+    }
+    IO.FS.writeFile path (textLog quorumTrace)
+    let accepted <- run "QUORUM" "0"
+    expect (accepted.exitCode == 0) s!"raw log CLI failed: {accepted.stderr}"
+    IO.FS.writeFile path (jsonLog failoverTrace)
+    let failover <- run "FAILOVER" "0"
+    expect (failover.exitCode == 0) s!"failover log CLI failed: {failover.stderr}"
+    let wrongKind <- run "QUORUM" "0"
+    expect (wrongKind.exitCode == 1) "CLI accepted wrong scenario"
+    IO.FS.writeFile path (textLog quorumTrace.dropLast)
+    let incomplete <- run "QUORUM" "0"
+    expect (incomplete.exitCode == 1) "CLI accepted missing completion"
+    let child <- IO.Process.spawn {
+      cmd := validator
+      args := #["--logs", "1", "QUORUM", "2000", path.toString]
+      stdout := .piped
+      stderr := .piped
+    }
+    IO.sleep 100
+    IO.FS.withFile path .append fun handle =>
+      handle.putStr (textLog [quorumTrace.getLast!])
+    let code <- child.wait
+    let error <- child.stderr.readToEnd
+    expect (code == 0) s!"CLI did not wait for appended completion: {error}"
+    IO.FS.writeFile path "RDP_TRACE {broken}\n"
+    let before <- IO.monoMsNow
+    let invalid <- run "QUORUM" "30000"
+    expect (invalid.exitCode == 1) "CLI accepted malformed trace JSON"
+    expect ((← IO.monoMsNow) - before < 5000) "CLI retried malformed input"
+    let missing <- IO.Process.output {
+      cmd := validator
+      args := #["--logs", "1", "QUORUM", "0", (directory / "missing").toString]
+    }
+    expect (missing.exitCode != 0) "CLI ignored unreadable log"
+    for args in [
+        #["--logs", "0", "QUORUM", "0", path.toString],
+        #["--logs", "1", "WRONG", "0", path.toString],
+        #["--logs", "1", "QUORUM", "-1", path.toString],
+        #["--logs", "1", "QUORUM", "0"]] do
+      let badArgs <- IO.Process.output { cmd := validator, args }
+      expect (badArgs.exitCode == 2) "CLI accepted invalid arguments"
+    IO.FS.writeFile path (String.join (quorumTrace.map fun event =>
+      (eventJson event).compress ++ "\n"))
+    let ndjson <- IO.Process.output { cmd := validator, args := #[path.toString] }
+    expect (ndjson.exitCode == 0) "existing ordered NDJSON interface was broken"
+
+def main : IO UInt32 := do
+  checkLogs
+  checkMultiNodeLogs
+  checkLogCLI
+  expect (validationSucceeds quorumTrace) "complete quorum trace was rejected"
+
+  let locations := ["A", "B"]
+  expect
+    (failedAt [startEvent locations "A", startEvent locations "B"] 2)
+    "incomplete multi-node trace was accepted"
+  expect
+    (failedAt [startEvent locations "A"] 1)
+    "incomplete single-node trace was accepted"
+  expect
+    (failedAt [startEvent locations "A", startEvent locations "A"] 2)
+    "duplicate start was accepted"
+  expect
+    (failedAt [startEvent ["A", "A"] "A"] 1)
+    "duplicate expected locations were accepted"
+  expect
+    (failedAt [{ startEvent ["A"] "A" with instanceId := "" }] 1)
+    "empty recovery instance was accepted"
+
+  let single := ["A"]
+  let start := startEvent single "A"
+  let gossipSend := sendEvent single 1 "send-gossip" "gossip:A" .gossiping
+  let missingCause := {
+    gossipEvent single 2 "receive-gossip" "missing" .voting with
+    causedBy := none
+  }
+  expect
+    (failedAt [start, gossipSend, missingCause] 3)
+    "receive without caused_by was accepted"
+
+  let wrongClass := {
+    voteEvent single 2 "receive-vote" "send-gossip" .voting with
+    pre := some .gossiping
+  }
+  expect
+    (failedAt [start, gossipSend, wrongClass] 3)
+    "vote consumed a gossip send"
+
+  let wrongTxid := {
+    gossipEvent single 2 "receive-gossip" "send-gossip" .voting with
+    txid := some { view := 9, seqno := 9 }
+  }
+  expect
+    (failedAt [start, gossipSend, wrongTxid] 3)
+    "gossip received a different TxID than its send"
+
+  let wrongPost := gossipEvent single 2 "receive-gossip" "send-gossip" .open
+  expect
+    (failedAt [start, gossipSend, wrongPost] 3)
+    "invalid gossip post-state was accepted"
+
+  let received := gossipEvent single 2 "receive-gossip" "send-gossip" .voting
+  let reusedCause := {
+    voteEvent single 3 "receive-vote" "send-gossip" .voting with
+    pre := some .voting
+  }
+  expect
+    (failedAt [start, gossipSend, received, reusedCause] 4)
+    "one send caused multiple receives"
+
+  let badSend := sendEvent single 1 "send-vote" "vote:A" .gossiping
+  expect
+    (failedAt [start, badSend] 2)
+    "Voting send was accepted while Gossiping"
+
+  let abortedTimeout := timeoutEvent single 1 .gossiping .gossiping
+  expect
+    (failedAt [start, abortedTimeout] 2)
+    "aborted empty-gossip timeout was accepted"
+
+  let throughOpen := quorumTrace.take 7
+  expect
+    (failedAt (throughOpen ++ [openEvent single 7 .quorum]) 8)
+    "one opening transition produced multiple open observations"
+  expect
+    (failedAt (quorumTrace.take 6) 6)
+    "trace with an unobserved opening effect was accepted"
+
+  let rejectedJson :=
+    "{\"instance\":\"x\",\"expected_locations\":[\"A\"],"
+      ++ "\"node\":\"A\",\"sequence\":0,\"kind\":\"gossip_rejected\","
+      ++ "\"pre\":\"GOSSIPING\",\"post\":\"GOSSIPING\"}"
+  expect (parseFails rejectedJson)
+    "unused rejection event remains in the trace format"
+
+  IO.println "all raw log, CLI, and strict trace replay checks passed"
+  pure 0
diff --git a/lean/disaster-recovery-trace/lake-manifest.json b/lean/disaster-recovery-trace/lake-manifest.json
new file mode 100644
index 00000000000..4a2b5828032
--- /dev/null
+++ b/lean/disaster-recovery-trace/lake-manifest.json
@@ -0,0 +1,138 @@
+{
+  "version": "1.2.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/leanprover-community/axiom-audit.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "46024e005996495c65ef609368e11ab39c4222e3",
+      "name": "axiomAudit",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "46024e005996495c65ef609368e11ab39c4222e3",
+      "inherited": false,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "type": "path",
+      "scope": "",
+      "name": "disaster_recovery",
+      "manifestFile": "lake-manifest.json",
+      "inherited": false,
+      "dir": "../disaster-recovery",
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/mathlib4.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+      "name": "mathlib",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.33.1",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+      "name": "LeanSearchClient",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+      "name": "importGraph",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+      "name": "proofwidgets",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+      "name": "aesop",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+      "name": "Qq",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+      "name": "batteries",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.33.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "disaster_recovery_trace",
+  "lakeDir": ".lake",
+  "fixedToolchain": false
+}
diff --git a/lean/disaster-recovery-trace/lakefile.toml b/lean/disaster-recovery-trace/lakefile.toml
new file mode 100644
index 00000000000..cebc96ce56d
--- /dev/null
+++ b/lean/disaster-recovery-trace/lakefile.toml
@@ -0,0 +1,30 @@
+name = "disaster_recovery_trace"
+version = "0.1.0"
+moreLeanArgs = ["-DwarningAsError=true"]
+lintDriver = "axiomAudit/\u00abaxiom-audit\u00bb"
+lintDriverArgs = ["--root", "DisasterRecoveryTrace"]
+defaultTargets = [
+  "DisasterRecoveryTrace",
+  "trace-checks",
+  "trace-validator",
+]
+
+[[require]]
+name = "disaster_recovery"
+path = "../disaster-recovery"
+
+[[require]]
+name = "axiomAudit"
+git = "https://github.com/leanprover-community/axiom-audit.git"
+rev = "46024e005996495c65ef609368e11ab39c4222e3" # v0.1.2
+
+[[lean_lib]]
+name = "DisasterRecoveryTrace"
+
+[[lean_exe]]
+name = "trace-checks"
+root = "TraceTests"
+
+[[lean_exe]]
+name = "trace-validator"
+root = "TraceMain"
diff --git a/lean/disaster-recovery-trace/lean-toolchain b/lean/disaster-recovery-trace/lean-toolchain
new file mode 100644
index 00000000000..a8afa7d1b02
--- /dev/null
+++ b/lean/disaster-recovery-trace/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.1
diff --git a/tests/e2e_operations.py b/tests/e2e_operations.py
index 3c3fb2ed8b0..3f478e92e51 100644
--- a/tests/e2e_operations.py
+++ b/tests/e2e_operations.py
@@ -38,6 +38,7 @@
 import infra.path
 import infra.platform_detection
 import infra.proc
+import infra.recovery_trace
 import infra.utils
 import suite.test_requirements as reqs
 from ccf.tx_id import TxID
@@ -2885,6 +2886,9 @@ def run_recovery_decision_protocol(const_args):
             assert (
                 recovery_type == '"Quorum"'
             ), f"Network self-healing open type was {recovery_type} instead of Quorum"
+            infra.recovery_trace.validate_recovery_trace_if_enabled(
+                recovered_network, args.label, "QUORUM"
+            )
 
 
 def run_recovery_decision_protocol_timeout_path(const_args):
@@ -2937,6 +2941,9 @@ def run_recovery_decision_protocol_timeout_path(const_args):
             assert (
                 recovery_type == '"Failover"'
             ), f"Network self-healing open type was {recovery_type} instead of Failover"
+            infra.recovery_trace.validate_recovery_trace_if_enabled(
+                recovered_network, args.label, "FAILOVER"
+            )
 
 
 def run_recovery_decision_protocol_multiple_timeout(const_args):
@@ -2989,6 +2996,9 @@ def run_recovery_decision_protocol_multiple_timeout(const_args):
                 node.refresh_network_state(verify_ca=False)
 
             assert len(recovered_network.get_joined_nodes()) == len(args.nodes)
+            infra.recovery_trace.validate_recovery_trace_if_enabled(
+                recovered_network, args.label, "FAILOVER"
+            )
 
 
 def run_read_ledger_on_testdata(args):
diff --git a/tests/infra/recovery_trace.py b/tests/infra/recovery_trace.py
new file mode 100644
index 00000000000..2341211741a
--- /dev/null
+++ b/tests/infra/recovery_trace.py
@@ -0,0 +1,73 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+# Licensed under the Apache 2.0 License.
+
+import logging
+import os
+import pathlib
+import subprocess
+
+TRACE_VALIDATOR_ENV = "CCF_LEAN_TRACE_VALIDATOR"
+LOG = logging.getLogger(__name__)
+
+
+def _validator_path():
+    configured = os.getenv(TRACE_VALIDATOR_ENV)
+    if configured:
+        return pathlib.Path(configured)
+    repository = pathlib.Path(__file__).resolve().parents[2]
+    return (
+        repository
+        / "lean"
+        / "disaster-recovery-trace"
+        / ".lake"
+        / "build"
+        / "bin"
+        / "trace-validator"
+    )
+
+
+def validate_recovery_trace(network, label, expected_open_kind, timeout=20):
+    nodes = [node for node in network.nodes if node.remote is not None]
+    log_paths = []
+    for node in nodes:
+        out_path, _ = node.get_logs()
+        if out_path is None:
+            raise FileNotFoundError(f"missing recovery trace log for {label}")
+        log_paths.append(out_path)
+
+    validator = _validator_path()
+    if not validator.is_file():
+        raise FileNotFoundError(
+            f"Lean trace validator not found at {validator}; set {TRACE_VALIDATOR_ENV}"
+        )
+    result = subprocess.run(
+        [
+            validator,
+            "--logs",
+            str(len(nodes)),
+            expected_open_kind,
+            str(round(timeout * 1000)),
+            *log_paths,
+        ],
+        text=True,
+        capture_output=True,
+        check=False,
+        timeout=timeout + 5,
+    )
+    if result.returncode != 0:
+        raise AssertionError(
+            f"Lean recovery trace validation failed for {label} ({log_paths}):\n"
+            f"{result.stdout}{result.stderr}"
+        )
+    LOG.info(result.stdout.strip())
+
+
+def validate_recovery_trace_if_enabled(network, label, expected_open_kind, timeout=20):
+    if not os.getenv(TRACE_VALIDATOR_ENV):
+        return None
+    return validate_recovery_trace(
+        network,
+        label,
+        expected_open_kind=expected_open_kind,
+        timeout=timeout,
+    )