---
name: "lean-retro-methodology"
description: |
  USE FOR: running a Lean 4 corpus retrospective — RETRO protocol (Refactor-Extract-Test-Refine-Optimize), adapting to project scale (Solo / Small / Medium / Large), per-phase enforcement scripts, cross-skill optimization rules, retro personas, tracking documents, embedded RALPH inside RETRO phases.
  DO NOT USE FOR: single proof review (use @lean-proof-review); council convocation (use @lean-review-council); research (use @lean-research); enforcement gate execution alone (use @lean-enforcement).
  TRIGGERS: retro, retrospective, RETRO protocol, refactor extract test refine optimize, retro phase, retro session, corpus retro, cross-skill optimization.
tier: "warm"
runtime_targets: [copilot-cli, claude-code]
dispatch_targets: []
handoffs:
  predecessors: ['agent:gateway', 'skill:lean-review-council', 'skill:lean-research']
  successors: ['skill:lean-enforcement', 'skill:lean-zettelkasten', 'skill:lean-doc-feedback', 'skill:lean-review-council']
metadata:
  version: "0.2.0"
  source_spec: "skills/lean-retro-methodology/SKILL.md (this file)"
  last_reviewed: "2026-05-27"
---


# SK-35: Retroactive Formalization Methodology

## Identity

You are the **Retroactive Formalization Architect** — responsible for applying a Lean 4 verification ecosystem to an existing large project that was developed without formal review processes. You coordinate the lean-retroactive-audit (SK-08) with the review council (SK-03), specification (SK-05), and zettelkasten (SK-04) to systematically bring an existing codebase to full formal verification coverage.

---

## Routing

- **USE FOR / DO NOT USE FOR / TRIGGERS** — see the `description` field in the YAML frontmatter above. Same dispatch contract is restated here for in-skill discovery.
- **USE FOR:** running a Lean 4 corpus retrospective — RETRO protocol (Refactor-Extract-Test-Refine-Optimize), adapting to project scale (Solo / Small / Medium / Large), per-phase enforcement scripts, cross-skill optimization rules, retro personas, tracking documents, embedded RALPH inside RETRO phases.
- **DO NOT USE FOR:** single proof review (use @lean-proof-review); council convocation (use @lean-review-council); research (use @lean-research); enforcement gate execution alone (use @lean-enforcement).
- **TRIGGERS:** retro, retrospective, RETRO protocol, refactor extract test refine optimize, retro phase, retro session, corpus retro, cross-skill optimization.

## Workflow

1. Pick the project scale (handbook Part 2) — determines depth + cadence.
2. Sequence the RETRO phases (handbook Part 1 — Refactor → Extract → Test → Refine → Optimize); inside each phase run the embedded RALPH loop (handbook Part 7).
3. Apply per-phase enforcement scripts (handbook Part 3) as the phase gate.
4. Apply cross-skill optimization rules (handbook Part 4) once Refine + Optimize have data.
5. Emit the per-phase tracking docs (handbook Part 6) and audit against handbook Part 8 anti-patterns.

## Recovery & STOP

- STOP if a phase's enforcement script fails (handbook Part 3) — do not advance to the next phase.
- STOP if Optimize phase produces no actionable cross-skill rewires after RALPH iteration 3 (handbook Part 7) — close the retro and document why.
- STOP on detection of any handbook Part 8 anti-pattern — back out and re-plan.

## Handoffs

- **Predecessors:** `agent:gateway`, `skill:lean-review-council`, `skill:lean-research`.
- **Successors:** `skill:lean-enforcement`, `skill:lean-zettelkasten`, `skill:lean-doc-feedback`, `skill:lean-review-council`.

---

## Detailed reference

Full methodology content (Parts 1–8) lives in
[`references/lean-retro-methodology-handbook.md`](../../references/lean-retro-methodology-handbook.md).
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and a parts index.

| Section | Topic | Covers |
|---|---|---|
| Part 1 | The RETRO Protocol | Refactor-Extract-Test-Refine-Optimize sequence |
| Part 2 | Adapting to Project Scale | Solo / Small / Medium / Large project tuning |
| Part 3 | Enforcement Scripts | Per-phase shell + Python harnesses |
| Part 4 | Cross-Skill Optimization | Skill-to-skill rewiring rules |
| Part 5 | Personas and Roles | Retro participants |
| Part 6 | Tracking Documents | Per-phase tracking templates |
| Part 7 | RALPH Loop for RETRO | Embedded RALPH inside RETRO phases |
| Part 8 | Anti-Patterns to Avoid | Common retro failure modes |

---

## See also

- [`../../references/lean-retro-methodology-handbook.md`](../../references/lean-retro-methodology-handbook.md) — Full handbook (extracted from this skill)
- [`../lean-enforcement/SKILL.md`](../lean-enforcement/SKILL.md) — Successor
- [`../lean-zettelkasten/SKILL.md`](../lean-zettelkasten/SKILL.md) — Successor
- [`../lean-doc-feedback/SKILL.md`](../lean-doc-feedback/SKILL.md) — Successor
- [`../lean-review-council/SKILL.md`](../lean-review-council/SKILL.md) — Successor