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: workflows/lean-squad.md
+1Lines changed: 1 addition & 0 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -581,6 +581,7 @@ This task is important because the value of any proof depends entirely on how fa
581
581
- One section per Lean file / target.
582
582
- For each modelled function or type, include a markdown table or enumerated list with: Lean name, Rust name, file + line reference, correspondence level, and a brief justification.
583
583
- Include links to the Rust source lines (use relative paths, e.g. `src/raft_log.rs#L42`).
584
+
- For each target, include a **Validation evidence** entry linking to whichever Task 8 artifact demonstrates correspondence: the Aeneas-generated Lean file (e.g. `formal-verification/lean/FVSquad/Aeneas/Generated/<Name>.lean`) if Route A was used, or the runnable test harness (e.g. `formal-verification/tests/<name>/`) if Route B was used. If neither exists yet, note that correspondence has not yet been independently validated.
584
585
- Summarise any known gaps or mismatches that should be resolved before trusting associated proofs.
585
586
-**Always** include a `## Last Updated` section at the top with the current UTC date/time and the HEAD commit SHA:
0 commit comments