[Lean Squad] Formal Verification Status

[github-actions]

🔬 Lean Squad — Formal Verification Status

Auto-maintained by the Lean Squad FV agent. Last updated: 2026-04-30.

At a Glance

Item	Value
FV Tool	Lean 4 (no Mathlib; will be re-added when first .lean file is written)
Targets identified	7
Targets with informal spec (Phase 2)	7
Lean spec files written (Phase 3)	0
Lean proofs attempted (Phase 5)	0
Confirmed bugs found	2
Design issues documented	5

Target Progress

#	Name	Phase	Status
1	ArgumentArity	2	Informal spec extracted
2	CommandLineParser.TryUnescape	2	Informal spec extracted
3	CommandLineParser.ParseOptionAndSeparators	2	Informal spec extracted
4	CommandLineOptionsValidator arity validation	2	Informal spec extracted (this run)
5	CommandLineParseResult.Equals	2	Informal spec extracted
6	ResponseFileHelper.SplitCommandLine	2	Informal spec extracted
7	TreeNodeFilter.MatchFilterPattern	2	Informal spec extracted

All 7 targets are now at Phase 2. The next major milestone is Task 3 (Lean 4 formal spec) for the highest-priority target — ArgumentArity.

Findings

Confirmed Bugs

#	Target	Description
BUG-1	TryUnescape	Single-char quote input (') → ArgumentOutOfRangeException via IndexOf(char, 1, -1)
BUG-2	TryUnescape	Single-char double-quote input (") → range exception from input[1..^1] on length-1 string

Design Issues

#	Target	Description
DI-1	SplitCommandLine	Unclosed opening quote silently discards all content
DI-2	SplitCommandLine	Adjacent quoted strings emit 2 tokens not 1
DI-3	ParseOptionAndSeparators	Empty option name not rejected: --:value produces currentOption="" silently
DI-4	ValidateOptionsArgumentArity	KeyNotFoundException risk if unknown option bypasses ValidateNoUnknownOptions
DI-5	ValidateOptionsArgumentArity	Options with Min > 0 that are absent from parse result are not detected here

Approach Notes

• Targets: All focus on the command-line infrastructure of Microsoft.Testing.Platform — pure functions with clear I/O contracts, ideal for formal verification.
• Lean toolchain: leanprover/lean4:v4.14.0, managed by elan. CI in .github/workflows/lean-proofs.yml.
• No Mathlib yet: lakefile.toml has no external dependencies until the first .lean file is written (reduces CI cost).
• Progress over perfection: sorry-guarded specs with proved invariants count as real progress.

Run History

Date	Run	Tasks	Outcome
2026-04-30	#25177606050	Task 2 + Task 9	Informal spec for CommandLineOptionsValidator arity validation; Mathlib removed from lakefile.toml; lake update step removed from CI. All 7 targets now at Phase 2.
2026-04-30	prior	Task 6 + Task 2	Correspondence review; informal specs for ParseOptionAndSeparators, ParseResult.Equals, SplitCommandLine.
2026-04-27	prior	Task 9 + Task 2	CI workflow improvements; TreeNodeFilter.MatchFilterPattern informal spec.
2026-04-24	prior	Task 1 + Task 9	FV infrastructure, research, ArgumentArity and TryUnescape informal specs.

Generated by 📐 Lean Squad, see workflow run.

---

🔬 Lean Squad — Formal Verification Status

Auto-maintained by the Lean Squad FV agent. Last updated: 2026-05-04.

At a Glance

Item	Value
FV Tool	Lean 4 + Mathlib
Targets identified	15
Targets with informal spec (Phase 2)	7
Lean spec files written (Phase 3)	0
Lean proofs attempted (Phase 5)	0
Confirmed bugs found	2
Design issues documented	5

Summary

The Lean Squad has been running multiple times and has built up a substantial pipeline of FV targets. Seven targets have informal specifications merged. Three more targets were added this run. Task 3 (Lean spec writing) remains blocked by the network-firewalled sandbox — elan/curl cannot reach GitHub releases. CI-based verification via leanprover/lean4-action is the established workaround.

Targets

#	Name	Phase	Spec	Notes
1	ArgumentArity	2	merged	Decidable properties; warm-up target
2	CommandLineParser.TryUnescape	2	merged	BUG-1, BUG-2 confirmed
3	CommandLineParser.ParseOptionAndSeparators	2	merged	Empty option name not rejected
4	CommandLineOptionsValidator arity	1	—	Next: Task 2
5	CommandLineParseResult.Equals	2	merged	All theorems decide-provable
6	ResponseFileHelper.SplitCommandLine	2	merged	Design issues documented
7	TreeNodeFilter.MatchFilterPattern	2	merged	Boolean algebra; induction proofs
8	PasteArguments.AppendArgument	1	—	Windows argv escaping
9	TimeSpanParser.TryParse	1	—	Suffix-dispatch parser
10	TreeNodeFilter.TokenizeFilter	1	—	Tokenizer
11	Sha256Hasher.ToCharsBuffer	1	—	Branchless hex encoding
12	ExtensionValidationHelper.ValidateUniqueExtension	1	—	Duplicate-UID detection
13	ValidationResult algebraic properties	1	—	NEW — tiny struct, all decide-provable
14	ValidateNoUnknownOptions	1	—	NEW — set-membership property
15	ValidateOptionsAreNotDuplicated	1	—	NEW — uniqueness over multi-map

Findings

Confirmed Bugs

• BUG-1 (TryUnescape): Single-char quote input ' → IndexOf(char, 1, -1) throws ArgumentOutOfRangeException.
• BUG-2 (TryUnescape): Single-char double-quote " → input[1..^1] range exception.

Design Issues

• SplitCommandLine: Unclosed opening quote at start silently discards all input content.
• SplitCommandLine: Adjacent quoted strings "a""b" emit 2 tokens, not 1.
• ParseOptionAndSeparators: Empty option name --:value produces currentOption="" silently.
• ValidateOptionsArgumentArity: KeyNotFoundException risk if unknown option bypasses ValidateNoUnknownOptions.
• ValidateOptionsArgumentArity: Absent required options (Min > 0 but option absent) not caught here; delegated to ValidateConfigurationAsync.

Approach Notes

• Lean 4 + Mathlib for all proofs.
• Pure functional Lean models of C# business logic, with explicit approximation notes.
• sorry used liberally early on; goal is correct theorem statements first.
• decide for concrete/finite types; omega for arithmetic; simp + induction for recursive structures.
• Lean toolchain blocked locally; CI runs via leanprover/lean4-action.

Run History

Run	Date	Tasks	Outcome
Run 25331082787	2026-05-04	Task 1 (T3 blocked) + Task Final	Added Targets 13–15 (ValidationResult, ValidateNoUnknownOptions, ValidateOptionsAreNotDuplicated); synced TARGETS.md phases with merged PRs. PR opened.
Run (prior)	2026-05-04	Task 1	Added Targets 13–15 (UnicodeCharacterUtilities, TestNodeUid, CommandLineOption) via PR lean-squad/task1-new-targets-2026-05-04-run2 (open).
Run (prior)	2026-05-04	Task 1	Added Targets 8–12 via PR #7849 (merged).
Run (prior)	2026-05-03	Task 2	TreeNodeFilter.MatchFilterPattern informal spec via PR #7934 (merged).
Run (prior)	2026-05-03	Task 9	FV docs validation + REPORT.md via PR #7936 (merged).
Run (prior)	2026-05-03	Task 9	Fix elan SHA256, cache ordering via PR #7924 (merged).
Run (prior)	2026-05-03	Task 2	CommandLineParseResult.Equals informal spec via PR #7918 (merged).
Run (prior)	2026-05-03	Task 2	ParseOptionAndSeparators informal spec via PR #7919 (merged).
Run (prior)	2026-05-03	Task 2	SplitCommandLine informal spec via PR #7899 (merged).
Run (prior)	2026-05-03	Task 9	CI skip guard + FVSquad scaffold via PR #7859 (merged).
Run (prior)	2026-04-30	Task 6	Correspondence review via merged PR.
Run (prior)	2026-04-30	Infrastructure	Initial FV infrastructure via PR #7799 (merged).

Generated by 📐 Lean Squad, see workflow run.