Remove the superseded Stateright disaster recovery model

[Amaury Chamayou (achamayou)]

Stack status

This is part 3/4 of the disaster recovery verification stack. Part 1, #8277, is merged. This PR is stacked on the open part 2, #8279, at commit 2e39b3108127bee3576e83ec0c5345d2bb723096.

The Temporary migration evidence check passed on that exact #8279 commit, including exhaustive Rust/Lean graph comparison for one, two, and three nodes. If the predecessor head changes, that evidence must pass again on the new head before this PR merges.

Summary

This PR removes the temporary migration evidence after #8279 established two deliberately different results:

1. Exact bounded graph equality between the legacy Rust/Stateright model and its Lean mirror for one, two, and three nodes.
2. A phase-only refinement from the canonical C++-aligned Lean model to the legacy Lean mirror. This is not a full bisimulation or data refinement.

Changes

• Delete the complete temporary lean/disaster-recovery-migration/ package.
• Delete the complete legacy tla/disaster-recovery/ Rust/Stateright project, including its temporary graph exporter.
• Remove the temporary migration-evidence job and the deleted Stateright path trigger from .github/workflows/lean.yml.
• Remove the legacy model-checking-self-healing-open job from .github/workflows/ci-verification.yml.
• Update .github/workflows/README.md to describe the remaining workflows.

The shared .github/workflows/lean.yml remains the repository's single Lean workflow. Its permanent canonical disaster recovery job runs on relevant pull requests. A proposed weekly trigger was removed after review because the toolchain and dependencies are pinned and this workflow performs no external trace validation.

Canonical model unchanged

There is no diff under lean/disaster-recovery/ from the current #8279 head. This PR does not alter the canonical model, proofs, executable checks, or package metadata validated by the predecessor.

Validation

• lake exe mk_all --check --lib DisasterRecovery
• lake build --wfail
• lake lint
• lake exe canonical-checks
• scripts/prettier-checks.sh
• scripts/ascii-checks.sh
• Parent diff audit confirming no changes under lean/disaster-recovery/

Part 4, #8282, adds C++ trace emission and Lean trace replay under lean/disaster-recovery-trace/.

[Heidi Howard (heidihoward)]

With one very minor exception, this PR simply deletes the old DR mode in stateright and the code to show equivalence to new lean mode, I see no reason not to merge when we are ready

[Copilot]

🔵 Needs a closer look

It is explicitly gated on stacked-PR evidence and full migration CI results that cannot be verified from this diff alone.

Pull request overview

This PR removes the now-superseded legacy disaster recovery model and the temporary Lean/Rust migration-evidence layer, leaving the canonical Lean disaster recovery model as the single maintained source of verification in the repo. It also updates CI workflows and workflow documentation to drop the removed jobs and triggers.

Changes:

• Deletes the legacy Rust/Stateright disaster recovery model project under tla/disaster-recovery/.
• Deletes the temporary Lean migration evidence package under lean/disaster-recovery-migration/.
• Removes the associated GitHub Actions jobs/triggers and updates workflow documentation accordingly.

Custom instructions used

None (no additional repository instruction files were loaded via tools).

File summaries

File	Description
tla/disaster-recovery/src/model.rs	Removed legacy Stateright actor/model implementation.
tla/disaster-recovery/src/main.rs	Removed legacy CLI (check/serve/export) entrypoint.
tla/disaster-recovery/src/export.rs	Removed legacy canonical graph exporter implementation.
tla/disaster-recovery/Readme.md	Removed documentation for the legacy Stateright model and exporter format.
tla/disaster-recovery/Cargo.toml	Removed legacy Rust crate manifest.
tla/disaster-recovery/Cargo.lock	Removed legacy Rust dependency lockfile.
tla/disaster-recovery/.gitignore	Removed legacy Rust build ignore rules (project deleted).
lean/disaster-recovery-migration/Tests.lean	Removed temporary semantic checks for the migration mirror.
lean/disaster-recovery-migration/README.md	Removed temporary migration package documentation.
lean/disaster-recovery-migration/Main.lean	Removed temporary migration model-checker executable entrypoint.
lean/disaster-recovery-migration/lean-toolchain	Removed pinned Lean toolchain for the temporary migration package.
lean/disaster-recovery-migration/lakefile.toml	Removed Lake configuration for the temporary migration package.
lean/disaster-recovery-migration/lake-manifest.json	Removed Lake manifest for the temporary migration package.
lean/disaster-recovery-migration/ExportMain.lean	Removed temporary migration exporter executable entrypoint.
lean/disaster-recovery-migration/DisasterRecoveryMigration/Refinement.lean	Removed temporary phase-refinement proof layer (bridge).
lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Model.lean	Removed Lean mirror of the legacy model (temporary bridge).
lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean	Removed temporary Lean BFS checker/exporter for legacy mirror.
lean/disaster-recovery-migration/DisasterRecoveryMigration.lean	Removed migration package root module.
lean/disaster-recovery-migration/compare.py	Removed Rust/Lean exhaustive graph comparison script (temporary evidence).
.github/workflows/README.md	Updated workflow documentation to drop references to removed DR migration/evidence jobs.
.github/workflows/lean.yml	Removed migration-evidence job and the tla/disaster-recovery/** PR path trigger; retains canonical Lean checks.
.github/workflows/ci-verification.yml	Removed the Self-Healing Open model-checking job which depended on the deleted legacy project.

Review details

• Files reviewed: 21/22 changed files
• Comments generated: 0
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.