Add Lean Squad formal verification agentic workflow

[Evangelink]

Lean Squad Formal Verification Agentic Workflow

This PR adds the Lean Squad workflow for progressive Lean 4 formal verification of the codebase.

Workflow Added

File	Trigger	Purpose
lean-squad.md	Every 8h + /lean-squad	Progressive Lean 4 formal verification

How It Works

The Lean Squad is a multi-phase automated agent that progressively applies formal verification:

1. Research & Target Identification — Survey codebase for FV-amenable targets
2. Informal Spec Extraction — Extract design intentions and informal contracts
3. Formal Spec Writing — Write Lean 4 type signatures and property statements
4. Implementation Extraction — Translate code to a Lean-verifiable functional model
5. Proof Assistance — Attempt proofs, find counterexamples, report bugs
6. Correspondence Review — Document how Lean models map to C# source
7. Proof Utility Critique — Assess value and coverage of proved properties
8. Correspondence Validation — Executable tests comparing source vs Lean model
9. CI Automation — Set up CI workflows for proof verification
10. Project Report — Maintain REPORT.md with mermaid diagrams

Key Features

• Weighted task selection: Tasks are selected based on current FV progress state
• Hard toolchain requirement: No .lean files submitted without successful lake build
• On-demand mode: /lean-squad <instructions> for specific tasks
• Persistent memory across runs for continuity
• Bug finding is success: Counterexamples are valuable outcomes

Safety

• Never submits unverified proofs
• Explicitly documents all model approximations
• One target per task per run for focused progress

Part of the agentic workflows setup series.

[Copilot]

Pull request overview

Adds a new gh-aw agentic workflow (“Lean Squad”) intended to drive progressive Lean 4 formal verification efforts over time (scheduled + on-demand).

Changes:

• Introduces .github/workflows/lean-squad.md workflow source defining phases/tasks, repo-memory usage, and safe-output limits.
• Adds a pre-step that inspects repo state and writes /tmp/gh-aw/task_selection.json to guide phase-weighted task selection.

Show a summary per file

File	Description
.github/workflows/lean-squad.md	New Lean Squad agentic workflow definition (frontmatter + prompt/instructions + state-based task selection step).

Copilot's findings

• Files reviewed: 1/1 changed files
• Comments generated: 4

[Copilot]

Copilot's findings

• Files reviewed: 1/1 changed files
• Comments generated: 5

[Copilot]

Copilot's findings

• Files reviewed: 3/4 changed files
• Comments generated: 3