r-irbe Lean 4 Retroactive Audit
Systematic methodology for applying the 5-member review council, Zettelkasten, and specification framework to a large existing Lean 4 codebase that was developed before these systems were in place.
Routing
- USE FOR: Apply the review council system retroactively to an existing large Lean 4 project. Use when onboarding an existing codebase to the council review framework. Covers module discovery, dependency analysis, incremental audit scheduling, baseline establishment, gap analysis, and the catch-up RALPH cycle for bringing an existing project to full review coverage.
- DO NOT USE FOR: building a new council (use @lean-review-council); single proof review (use @lean-proof-review); RETRO methodology (use @lean-retro-methodology).
- TRIGGERS: retroactive audit, council onboarding, existing project audit, legacy Lean review.
Workflow
- Survey the existing project: count theorems, sorries, native_decide, axiom totals, council coverage gaps.
- Pick the audit playbook from the body matching the project scale (Solo / Small / Medium / Large).
- Execute the audit; produce a per-module readiness report with sequencing for council onboarding.
- Hand off: to
@lean-review-councilfor the first council session, to@lean-retro-methodologyfor RETRO, to@lean-zettelkasten.
Recovery & STOP
- STOP if the project is new — delegate to
@lean-specificationto start from scratch. - STOP if the audit reveals architectural blockers — request HITL strategy decision.
- STOP if scope drifts into per-proof review — delegate single-proof items to
@lean-proof-review.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-review-council,skill:lean-retro-methodology,skill:lean-zettelkasten.
Detailed reference
Full content for lean-retroactive-audit lives in
references/lean-retroactive-audit-handbook.md.
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and the parts index.
| Section | Topic |
|---|---|
| Part 1 | The Retroactive Challenge |
| Part 2 | Phase 0: Discovery |
| Part 3 | Phase 1: Baseline Establishment |
| Part 4 | Phase 2: Incremental Deep Audit |
| Part 5 | Phase 3: Gap Analysis and Extension |
| Part 6 | Phase 4: Steady-State Transition |
| Part 7 | Parallel Audit Dispatch |
See also
../../references/lean-retroactive-audit-handbook.md— Full handbook (extracted from this skill)../lean-review-council/SKILL.md— Successor../lean-retro-methodology/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor