Remove the superseded Stateright disaster recovery model

.github/workflows/README.md

@@ -79,7 +79,7 @@ File: `codeql-analysis.yml`
 
 # Continuous Verification
 
-Runs the standard model checking, simulation, trace validation, counterexample, and disaster recovery jobs each week.
+Runs the standard model checking, simulation, trace validation, and counterexample jobs each week.
 
 File: `ci-verification.yml`
 3rd party dependencies: None
@@ -114,10 +114,6 @@ 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 temporary migration-evidence job builds and audits the Lean mirror of the
-legacy Rust/Stateright disaster recovery model, exercises both implementations,
-and exhaustively compares their complete graphs for up to three nodes.
-
 File: `lean.yml`
 3rd party dependencies: None
 

.github/workflows/ci-verification.yml

@@ -242,25 +242,3 @@ jobs:
           name: tlc-trace-validation-consensus
           path: |
             tla/traces/*
-
-  model-checking-self-healing-open:
-    name: Model Checking - Self-Healing Open
-    runs-on: [self-hosted, 1ES.Pool=gha-vmss-d16av6-ci]
-    container:
-      image: mcr.microsoft.com/azurelinux/base/core:3.0
-      options: --user root --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE
-
-    steps:
-      - name: "Checkout dependencies"
-        shell: bash
-        run: |
-          gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY
-          tdnf -y update
-          tdnf -y install ca-certificates git
-
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-      - name: Install Stateright dependencies
-        run: |
-          tdnf install -y cargo
-
-      - run: cd tla/disaster-recovery && cargo run check

.github/workflows/lean.yml

@@ -4,7 +4,6 @@ on:
   pull_request:
     paths:
       - "lean/**"
-      - "tla/disaster-recovery/**"
       - ".github/workflows/lean.yml"
 
 concurrency:
@@ -46,55 +45,3 @@ jobs:
           lake build --wfail
           lake lint
           lake exe canonical-checks
-
-  migration-evidence:
-    name: Temporary migration evidence
-    runs-on: ubuntu-latest
-    timeout-minutes: 90
-
-    steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-
-      - name: Install Lean and Rust
-        shell: bash
-        run: |
-          set -euo pipefail
-          sudo apt-get update
-          sudo apt-get install -y elan
-          elan toolchain install "$(cat lean/disaster-recovery-migration/lean-toolchain)"
-          rustup toolchain install stable --profile minimal
-          rustup default stable
-
-      - name: Build and check Rust model
-        working-directory: tla/disaster-recovery
-        shell: bash
-        run: |
-          set -euo pipefail
-          cargo check --locked
-          cargo build --locked
-          cargo run --quiet --locked -- --nodes 2 check
-
-      - name: Restore Mathlib cache
-        working-directory: lean/disaster-recovery-migration
-        shell: bash
-        run: |
-          set -euo pipefail
-          lake exe cache get
-
-      - name: Build and check migration model
-        working-directory: lean/disaster-recovery-migration
-        shell: bash
-        run: |
-          set -euo pipefail
-          lake exe mk_all --check --lib DisasterRecoveryMigration
-          lake build --wfail
-          lake lint
-          lake exe migration-semantic-checks
-          lake exe migration-model-checker --nodes 3
-
-      - name: Compare complete Rust and Lean graphs
-        working-directory: lean/disaster-recovery-migration
-        shell: bash
-        run: |
-          set -euo pipefail
-          python3 compare.py --nodes 1 2 3