You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/lean-squad.md
+46-13Lines changed: 46 additions & 13 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,6 +1,6 @@
1
1
# 🔬 Lean Squad
2
2
3
-
The [Lean Squad workflow](../workflows/lean-squad.md?plain=1) is a [GitHub Agentic Workflow](https://github.blog/ai-and-ml/automate-repository-tasks-with-github-agentic-workflows/) that applies Lean 4 formal verification to your codebase progressively and optimistically — without requiring any prior FV expertise. Each run it selects tasks weighted to the current phase of FV progress, from initial research all the way through to completed proofs. Maybe it finds a bug; maybe it proves something; either way, it makes forward progress.
3
+
The [Lean Squad workflow](../workflows/lean-squad.md?plain=1) is a [GitHub Agentic Workflow](https://github.blog/ai-and-ml/automate-repository-tasks-with-github-agentic-workflows/) that applies Lean 4 formal verification to your codebase progressively and optimistically — without requiring any prior FV expertise. Each run it selects tasks weighted to the current phase of FV progress, from initial research all the way through to completed proofs, correspondence reviews, project reports, and even a LaTeX conference paper. Maybe it finds a bug; maybe it proves something; either way, it makes forward progress.
4
4
5
5
## Installation
6
6
@@ -24,15 +24,19 @@ graph LR
24
24
A --> T3[Task 3: Formal Spec Writing]
25
25
A --> T4[Task 4: Implementation Extraction]
26
26
A --> T5[Task 5: Proof Assistance]
27
-
A --> T6[Task 6: Maintain Open Lean Squad PRs]
27
+
A --> T6[Task 6: Correspondence Review]
28
+
A --> T7[Task 7: Proof Utility Critique]
29
+
A --> T8[Task 8: Correspondence Validation]
30
+
A --> T9[Task 9: CI Automation]
28
31
A --> T10[Task 10: Project Report]
29
-
T1 & T2 & T3 & T4 & T5 & T6 & T10 --> T7[Task 7: Update FV Status Issue]
A deterministic pre-step counts FV artifacts in the repository (Lean files, spec docs, open issues and PRs) and computes a **phase-weighted probability** for each task. Two tasks are drawn and communicated to the agent; the agent confirms them against its memory and executes them. Task 7 (status update) always runs. All notes, targets, choices, and progress live in persistent **repo-memory** so each run builds on the last.
37
+
A deterministic pre-step counts FV artifacts in the repository (Lean files, spec docs, open issues and PRs) and computes a **phase-weighted probability** for each task. Two tasks are drawn and communicated to the agent; the agent confirms them against its memory and executes them. Task Final (status update) always runs. All notes, targets, choices, and progress live in persistent **repo-memory** so each run builds on the last.
34
38
35
-
The weighting scheme adapts automatically: when no FV work exists Task 1 dominates; once research is done Task 2 rises; as informal specs accumulate Task 3 gains weight; and so on up to proofs.
39
+
The weighting scheme adapts automatically: when no FV work exists Task 1 dominates; once research is done Task 2 rises; as informal specs accumulate Task 3 gains weight; and so on up to proofs. Once implementation models exist, Task 8 becomes available and is weighted heavily when no runnable correspondence tests exist yet.
Attempts to prove the stated propositions using Lean 4 tactics (`decide`, `omega`, `simp`, `linarith`, `ring`, `induction`, etc.). When a proof obligation cannot be closed, investigates whether the spec or the implementation is wrong. If a **counterexample** is found refuting a property, files a bug issue with the failing case, the expected property, and the impact. Proved theorems have their `sorry` removed; hard ones get a comment explaining the obstacle. Produces a PR with real progress.
66
70
67
-
### Task 6: Maintain Open Lean Squad PRs
71
+
### Task 6: Correspondence Review
68
72
69
-
Weight proportional to the number of open Lean Squad PRs.
73
+
Default weighting: critical when implementations exist but no correspondence doc.
70
74
71
-
Reviews open `[Lean Squad]` PRs, fixes CI failures (Lean syntax errors, `lake build` failures), and resolves merge conflicts. Stale or stuck PRs get a comment explaining the blocker.
75
+
For each Lean file containing an implementation model, reviews how faithfully the model corresponds to the actual source code. Assesses each definition's correspondence level (*exact*, *abstraction*, *approximation*, or *mismatch*), documents all known divergences with file/line references, and evaluates the impact on proof validity. Produces or updates `formal-verification/CORRESPONDENCE.md` as a PR. Flags any mismatches that invalidate proved theorems and opens issues for them.
72
76
73
-
### Task 7: Update Lean Squad Status Issue *(always)*
77
+
### Task 7: Proof Utility Critique
74
78
75
-
Maintains a single `[Lean Squad] Formal Verification Status` issue as a continuously-updated dashboard with an at-a-glance table (one row per target, showing current phase and status), summary narrative, findings section (bugs found, counterexamples), approach notes, and a prepended run history entry for every run.
79
+
Default weighting: critical when proofs exist but no critique doc.
80
+
81
+
Steps back to honestly assess whether the FV work is actually useful — are the proved properties meaningful, at the right level of abstraction, and likely to catch real bugs? Evaluates each theorem's level, bug-catching potential, coverage, and strength. Identifies the highest-value gaps and recommends what to prove next. Optionally reviews the conference paper (`paper.tex`) as a critical reviewer and includes actionable feedback. Produces or updates `formal-verification/CRITIQUE.md` as a PR.
Default weighting: available once implementation models exist; weighted highly when no runnable correspondence tests exist.
86
+
87
+
Validates that the Lean implementation model corresponds to the source code using one of two routes. Route A uses the Charon + Aeneas toolchain to automatically generate Lean 4 code from Rust source, producing a mechanically-derived model that can be bridged to the hand-written one. Route B writes and runs executable correspondence tests that exercise the source implementation and the Lean model on the same fixtures, which may require building a small standalone harness or copied test project under `formal-verification/tests/`. The task always prefers concrete, executed evidence over hand-wavy similarity claims.
88
+
89
+
### Task 9: CI Automation
90
+
91
+
Default weighting: critical when Lean files exist but no CI; regular check otherwise.
92
+
93
+
Sets up and maintains `.github/workflows/lean-ci.yml` and, when applicable, CI for Task 8 artifacts such as `aeneas-generate.yml` or runnable correspondence-test workflows. Audits CI health, checks for persistent failures, verifies cache effectiveness, and fixes broken workflows.
76
94
77
95
### Task 10: Project Report
78
96
79
97
Default weighting: important once proofs exist; available once Lean specs exist.
80
98
81
99
Creates and incrementally maintains `formal-verification/REPORT.md` — a comprehensive, reader-friendly project report summarising the entire FV effort. Uses mermaid diagrams extensively to visualise proof architecture, dependency layers, modelling choices, the main proof chain, and project timeline. Includes a mandatory Findings section documenting any bugs found (with counterexamples and issue links), formulation issues caught during development, and interesting structural discoveries. The report is updated incrementally each run rather than rewritten from scratch.
82
100
101
+
### Task 11: Conference Paper
102
+
103
+
Default weighting: important once proofs exist; only available once proofs exist.
104
+
105
+
Writes and maintains a LaTeX conference paper under `formal-verification/paper/` using a standard ACM (`acmart`) or IEEE (`IEEEtran`) template, targeting an 11-page limit. The paper covers methodology, findings, proof architecture, modelling choices, and lessons learned. Includes a Lean 4 listing style for code examples. The compiled PDF (`paper.pdf`) is committed to the repository and kept up to date. Each run updates the paper incrementally — adding new theorems, findings, and revised assessments. Requires `texlive` for compilation (installed automatically). Produces `paper.tex`, `paper.bib`, and `paper.pdf` as a PR.
106
+
107
+
### Task Final: Update Lean Squad Status Issue *(always)*
108
+
109
+
Maintains a single `[Lean Squad] Formal Verification Status` issue as a continuously-updated dashboard with an at-a-glance table (one row per target, showing current phase and status), summary narrative, findings section (bugs found, counterexamples), approach notes, and a prepended run history entry for every run.
110
+
83
111
## What Gets Created
84
112
85
113
| Artifact | Location | Description |
@@ -88,9 +116,14 @@ Creates and incrementally maintains `formal-verification/REPORT.md` — a compre
88
116
| Target list |`formal-verification/TARGETS.md`| Prioritised targets with phase status |
0 commit comments