[Lean Squad] Formal Verification Status

[github-actions]

🔬 Lean Squad — automated formal verification for this repository.

At a Glance

Target	Phase	Status	File
RingBuffer	Phase 5	✅ 26 theorems	RingBuffer.lean
ResultEx	Phase 5	✅ 19 theorems	ResultEx.lean
RetryPolicy	Phase 5	✅ 13 theorems	RetryPolicy.lean
RestartPolicy	Phase 5	✅ 10 theorems	RestartPolicy.lean
Affordances	Phase 5	✅ 19 theorems	Affordances.lean
EvalPipeline	Phase 5	✅ 20 theorems	EvalPipeline.lean
HotReloadState	Phase 5	✅ 30 theorems	HotReloadState.lean
SessionLifecycle	Phase 5	✅ 16 theorems	SessionLifecycle.lean
Theme	Phase 5	✅ 21 theorems	Theme.lean
Composition (cross-file)	Phase 5	✅ 12 theorems	Composition.lean
PhaseTransition (state machine)	Phase 5	✅ 11 theorems	PhaseTransition.lean
SmartReset	Phase 5	✅ 8 theorems	SmartReset.lean
SageFsError (error classification)	Phase 5	✅ 23 theorems	SageFsError.lean
SseReplayBuffer (SSE reconnect replay)	Phase 5	✅ 19 theorems	SseReplayBuffer.lean
FsiRewrite (FSI use→let rewrite)	Phase 5	✅ 19 theorems	FsiRewrite.lean
TimeTravel (navigation state machine)	Phase 5	✅ 30 theorems	TimeTravel.lean
BinaryFormat.Crc32	Phase 5	✅ 16 theorems	BinaryFormat.lean
WorkflowTypes.SessionWorkflow	Phase 1	⬜ Research identified	—
ValidTimeout	Phase 1	⬜ Research identified	—

Summary

The SageFs FV project now has 312 theorems across 17 Lean files, 0 sorry (lake build passes with Lean 4.30.0-rc2). This run (Tasks 3+4+5+6) completed the Lean spec for BinaryFormat.Crc32 — the project's first algorithmic target (pure CRC-32 implementation with standard test vector 0xCBF43926 verified). Also updated CORRESPONDENCE.md with a full BinaryFormat section and corrected an error in the informal spec (CRC-32 of [0x00] is 0xD202EF8D, not 0x2144DF1C).

Findings

• 🌟 crc32_test_vector: CRC-32 of "123456789" = 0xCBF43926 — the universally agreed standard test vector passes by native_decide, confirming the Lean model matches the ISO 3309 polynomial exactly
• 🌟 crc32_slicing_consistency: Proved that crc32Compute (pfx ++ data ++ sfx) pfx.length data.length = crc32All data — slice correctness via Lean stdlib List.drop/List.take lemmas
• ⚠️ Informal spec correction: binaryformat_crc32_informal.md stated CRC-32 of [0x00u] = 0x2144DF1Cu; the correct standard value is 0xD202EF8Du. This was a copy-paste error in the informal spec.
• No implementation bugs found in any target so far.

Approach Notes

• Tool: Lean 4 (v4.30.0-rc2), stdlib only (CI firewall blocks lakecache/Mathlib)
• Build: cd formal-verification/lean && lake build
• CI: lean-ci.yml ✅ | fv-correspondence-tests.yml ✅
• Key tactics: native_decide, omega, simp/simp only, decide, cases, rfl

Run History

2026-05-12 01:20 UTC — Run

• 📋 Task 3+4+5 (Formal Spec + Implementation + Proofs): BinaryFormat.lean — 16 theorems, 0 sorry
• 📋 Task 6 (Correspondence Review): Updated CORRESPONDENCE.md with BinaryFormat section; corrected informal spec error for [0x00] CRC value
• ✅ lake build PASSED — 19 jobs, 0 sorry, Lean 4.30.0-rc2 (312 total theorems across 17 files)
• 📝 PR created: BinaryFormat.Crc32 Lean spec + correspondence review

2026-05-11 17:10 UTC — Run

• 📋 Task 1 (Research): 3 new targets identified — BinaryFormat.Crc32 (HIGH), WorkflowTypes.SessionWorkflow (HIGH), ValidTimeout (MEDIUM)
• 📋 Task 2 (Informal Spec): specs/binaryformat_crc32_informal.md — 7 properties, 2 loop invariants, standard test vectors, slicing property, proof strategy
• 📝 PR created: Task 1+2 research + informal spec (merged as [Lean Squad] feat(fv): identify 3 new FV targets + BinaryFormat.Crc32 informal spec (Task 1+2, run 25685202317) #116)

2026-05-11 09:41 UTC — Run

• 📋 Task 3 (Formal Spec): TimeTravel.lean — 30 theorems, 0 sorry
• 📋 Task 6 (Correspondence Review): Updated CORRESPONDENCE.md with TimeTravel section
• 🔀 Consolidated open PRs into PR [Lean Squad] feat(fv): TimeTravel formal spec + consolidate all in-flight FV work (16 modules, 296 theorems) #115 (merged as TimeTravel + all prior work, 296 theorems)
• ✅ lake build PASSED

2026-05-09 16:35 UTC — Run

• 📋 Task 9 (CI Audit): Fixed fv-correspondence-tests.yml checkout@v5→v4
• 📋 Task 2 (Informal Spec): timetravel_informal.md

2026-05-08 17:01 UTC — Run

• 📋 Task 2 (Informal Spec): ssereplaybuffer_informal.md
• 📋 Task 5 (Proof Assistance): SseReplayBuffer.lean — 19 theorems, 0 sorry

2026-05-08 09:00 UTC — Run

• 📋 Task 4+5: SageFsError.lean — 26 theorems, 0 sorry

2026-05-07 09:15 UTC — Run

• 📋 Task 10+11: REPORT.md + paper/paper.tex created

2026-05-07 01:20 UTC — Run

• 📋 Task 5: PhaseTransition.lean — 14 theorems

2026-05-06 16:52 UTC — Run

• 📋 Task 5: Composition.lean — 12 cross-file theorems

Generated by 📐 Lean Squad, see workflow run. Learn more.

To install this agentic workflow, run

gh aw add githubnext/agentics/workflows/lean-squad.md@13377ddf7e35c2b6e47aa58f45acb228fba902c8

---

🔬 Lean Squad — automated formal verification for this repository.

At a Glance

Target	Phase	Status	File
RingBuffer	Phase 5	✅ 20 theorems	RingBuffer.lean
ResultEx	Phase 5	✅ 17 theorems	ResultEx.lean
RetryPolicy	Phase 5	✅ 13 theorems	RetryPolicy.lean
RestartPolicy	Phase 5	✅ 9 theorems	RestartPolicy.lean
Affordances	Phase 5	✅ 19 theorems	Affordances.lean
EvalPipeline	Phase 5	✅ 20 theorems	EvalPipeline.lean
HotReloadState	Phase 5	✅ 23 theorems	HotReloadState.lean
SessionLifecycle	Phase 5	✅ 16 theorems	SessionLifecycle.lean
Theme	Phase 5	✅ 20 theorems	Theme.lean
Composition	Phase 5	✅ 12 theorems	Composition.lean
PhaseTransition	Phase 5	✅ 14 theorems	PhaseTransition.lean
SmartReset	Phase 5	✅ 8 theorems	SmartReset.lean
SageFsError	Phase 5	✅ 23 theorems	SageFsError.lean
SseReplayBuffer	Phase 5	✅ 19 theorems	SseReplayBuffer.lean
FsiRewrite	Phase 5	✅ 17 theorems + 52 tests	FsiRewrite.lean
TimeTravel	Phase 5	✅ 30 theorems	TimeTravel.lean
BinaryFormat.Crc32	Phase 5	✅ 16 theorems + 28 tests	BinaryFormat.lean
WorkflowTypes.SessionWorkflow	Phase 5	✅ 20 theorems	WorkflowTypes.lean
ValidTimeout	Phase 1	⬜ Research done, no spec yet	—
DirectoryConfig.LoadStrategy	Phase 2	🔄 Informal spec written	specs/directoryconfig_loadstrategy_informal.md

316 theorems · 18 Lean files · 0 sorry · Lean 4.30.0-rc2 · stdlib-only

Summary

316 theorems proved across 18 Lean 4 files, zero sorry. The project covers the full spectrum of SageFs components: ring buffer correctness, error classification, session lifecycle safety, access control, hot-reload state machine, retry policies, time travel, CRC-32 conformance, and workflow constraints. The landmark recent result is no_hotReload_and_fullRepl in WorkflowTypes.lean, which proves the illegal "hot reload + full REPL" combination is structurally unrepresentable. Two targets remain: ValidTimeout (T19, Phase 1) and DirectoryConfig.LoadStrategy (T20, Phase 2 — informal spec written this run). No implementation bugs have been found in the F# source.

Findings

🌟 Structural findings

• no_hotReload_and_fullRepl (WorkflowTypes.lean): No SessionWorkflow value can simultaneously have hot-reload active and full REPL capability. This is structurally unrepresentable — not just runtime-guarded.
• toState_never_uninitialized (SessionLifecycle.lean): Uninitialized is unreachable from toState — confirms the sentinel design.
• eval_cannot_fault_directly (PhaseTransition.lean): Evaluation failure → Ready, never Faulted directly.
• send_fsharp_code_iff_ready_phase (Composition.lean): System-level evaluation gate proved end-to-end across SessionLifecycle and Affordances.

📝 Spec correction

• BinaryFormat CRC([0x00]): Initial informal spec stated 0x2144DF1C. Correct value is 0xD202EF8D (confirmed by native_decide + standard CRC-32 tables). Documented in CORRESPONDENCE.md §D3.

✅ No implementation bugs found

All proved properties hold for the Lean models of the F# source.

Approach Notes

• Tool: Lean 4 (stdlib-only; no Mathlib — CI firewall blocks lakecache/mathlib downloads)
• Toolchain: leanprover/lean4:v4.30.0-rc2 (pinned in lean-toolchain)
• Correspondence tests: 3 harnesses (RingBuffer 52 tests, FsiRewrite 52 tests, BinaryFormat 28 tests)
• Key abstractions: async/Task → pure synchronous functions; payload fields erased from error tags; snapshot contents abstracted; OS path separators abstracted
• CI: lean-ci.yml (lake build on all PRs/pushes) + fv-correspondence-tests.yml (F# test harnesses)

Run History

2026-05-13 09:30 UTC — Run

• 📋 Task 7 completed: full proof utility critique of all 18 Lean files (316 theorems)
  • Updated CRITIQUE.md: new theorem entries T12–T18, new positive findings, new concerns
  • New concern: SmartReset async model not capturing cancellation
  • New positive finding: crc32_test_vector confirms CRC-32 standard conformance
• 📋 Task 2 completed: informal spec for T20 DirectoryConfig.LoadStrategy
  • specs/directoryconfig_loadstrategy_informal.md created
  • T20 advanced to Phase 2; Lean spec (Task 3) is the next step
• 📝 PR created: feat(fv): proof utility critique (Task 7) + DirectoryConfig informal spec (Task 2)

2026-05-12 17:00 UTC — Run

• 🔬 Proved: 20 theorems in WorkflowTypes.lean (T18, 0 sorry)
• 🌟 no_hotReload_and_fullRepl: illegal state structurally unrepresentable
• 📝 PR created: [Lean Squad] feat(fv): WorkflowTypes.SessionWorkflow — 20 theorems, 0 sorry (Task 2+5) #121 — WorkflowTypes.SessionWorkflow (Task 2+5)

2026-05-12 09:30 UTC — Run

• 📋 Task 1: TARGETS.md updated (T18-T20 added), RESEARCH.md extended
• 📋 Task 10: REPORT.md updated to 296 theorems / 17 files
• 📝 PR created: [Lean Squad] feat(fv): update research targets + project report (Task 1+10, 17 files, 296 theorems) #120 — research + report update

2026-05-12 01:20 UTC — Run

• 🔬 Proved: 16 theorems in BinaryFormat.lean (T17, 0 sorry)
• 🌟 crc32_test_vector: CRC-32("123456789") = 0xCBF43926 confirmed by native_decide
• 📝 Spec correction: CRC([0x00]) = 0xD202EF8D (not 0x2144DF1C)
• 📝 PR created: [Lean Squad] feat(fv): BinaryFormat.Crc32 Lean spec + correspondence review (Task 3+4+5+6, 16 theorems, 0 sorry) #117 — BinaryFormat.Crc32 (Task 3+4+5+6)

Generated by 📐 Lean Squad, see workflow run. Learn more.

To install this agentic workflow, run

gh aw add githubnext/agentics/workflows/lean-squad.md@13377ddf7e35c2b6e47aa58f45acb228fba902c8