[Amaury Chamayou (achamayou)]

Motivation

Run Lean package checks concurrently in isolated workspaces instead of serially.

Implementation summary

A reusable workflow checks all five packages in a fail-fast-disabled matrix, with isolated dependency caches. Raft and KV captures and replay run independently; a final gate requires every check to pass. Existing proof, axiom, formatting, lint, and fixture checks remain. KV proof references and formatter coverage were updated.

Observed CI timings: 65m40s serial to 9m04s with the matrix, an 86% decrease in elapsed time.

Safety and compatibility

No production runtime, protocol, API, or toolchain changes. Kernel and axiom checks remain enabled.

[Copilot]

🔵 Needs a closer look

Hosted validation is still needed to verify reusable-workflow failure/cancellation aggregation and executable compatibility across producer/replay runners, which local checks and source inspection cannot establish.

No open issues 🎉

What changed in this PR

This PR moves CCF’s Lean checks from serial execution to isolated concurrent jobs, preserving existing validation while allowing native Raft replay to proceed independently of unrelated packages. Performance gains remain unmeasured.

Changes:

• Introduces a reusable package workflow with isolated checkouts and package-specific validation.
• Separates Raft replay using a permission-preserving executable artifact with integrity and runtime checks.
• Retains the Lean models and proofs gate, requiring successful prerequisites and checking package inventory.

Custom instructions used

Applied the supplied CCF repository guidance; no additional instruction files were loaded.

File	Description
lean/​disaster-recovery/​README.md	Documents package isolation, aggregate gating, and concurrency tradeoffs.
lean/​ccf-raft/​replay/​README.md	Documents independent captures, executable transfer, and replay validation.
.github/​workflows/​lean.yml	Orchestrates concurrent package checks, downstream replay, and the final gate.
.github/​workflows/​lean-package.yml	Adds reusable package validation and Raft executable packaging.

_{Review effort: Balanced}