Lean retro methodology

Skill r-irbe/proof-skills/skills/lean-retro-methodology

APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.

Install

npx -y skills add r-irbe/proof-skills --skill lean-retro-methodology

Assembled 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.

What its author says it does

Copied from the file, not written here

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.

SKILL.md

4.9 KB, as published. Nobody here has run it

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

Pick the project scale (handbook Part 2) — determines depth + cadence.
Sequence the RETRO phases (handbook Part 1 — Refactor → Extract → Test → Refine → Optimize); inside each phase run the embedded RALPH loop (handbook Part 7).
Apply per-phase enforcement scripts (handbook Part 3) as the phase gate.
Apply cross-skill optimization rules (handbook Part 4) once Refine + Optimize have data.
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. 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