Lean retroactive audit
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.From its SKILL.md
npx -y skills add r-irbe/proof-skills --skill lean-retroactive-auditAssembled from the repository path, not quoted from the project. Check it against their README if it does not work.
One thing to look at
- 2 stars2 stars. Stars are a popularity signal and not a quality one, but at this level it is likely that nobody has read this closely except its author, and you would be relying on your own review.
SKILL.md
3.8 KB, 707 tokens by cl100k_base, as published. Nobody here has run it
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
What ships with it
Read from the repository
Just SKILL.md. No reference files, no scripts.