[Lean Squad] feat(fv): Task 2 + Task 9 — arity validator informal spec + sorry regression guard

[Evangelink]

🔬 Lean Squad — automated formal verification agent run #25239813116.

---

Changes

Task 2 — Informal Spec: CommandLineOptionsValidator Arity Validation

New file: formal-verification/specs/commandlineoptionsvalidator_arity_informal.md

This spec covers ValidateOptionsArgumentArity, the private static method that checks whether each option in the parse result was given the right number of arguments:

• Context: Called as step 6 of the 8-step validation pipeline; assumes step 5 (unknown-option check) already passed.
• Core property: Arity is the sum of argument counts across all occurrences of the same option name.
• 8 postconditions: completeness, soundness, error-message coverage, empty-list validity, no-arg options, multi-occurrence accumulation, unknown-option absence, order-independence.
• 3 invariants: error-message monotonicity, arity bound tightness, special-case message uniqueness.
• 7 edge cases including the key design gap (EC5): options with Min > 0 that are absent from the parse result are not caught here — delegated to ValidateConfigurationAsync (step 8).
• 4 open questions including the pipeline ordering dependency (OQ-3) and Int32.MaxValue overflow concern (OQ-2).
• Lean 4 modelling notes: effectiveArity models naturally as a grouped-sum function; main theorem is a logical equivalence; P4 provable by simp.

TARGETS.md updated: target 4 advances from phase 1 → phase 2.

Task 9 — CI: Sorry Regression Guard

Modified file: .github/workflows/lean-proofs.yml

Three new steps added (all guarded by lean_count != '0'):

1. Improved proof summary — sorry label now shows ✅ 0 (fully proved) vs ⚠️ N (stubs remaining) for clearer at-a-glance status.

2. Sorry regression guard — enforces a hard threshold of 200 sorry lines total (generous for development phase). On pull-request events, compares against the base branch and emits:

   • ::warning if the PR increases sorry count (encourages replacing stubs with proofs)
   • ::notice if the PR decreases sorry count 🎉
   • Hard exit 1 only if total exceeds 200

3. Debug artifact check — warns on #eval commands in committed .lean files (common development leftover that shouldn't ship).

---

Checklist

• No changes to C# production code
• No .lean files (Lean toolchain unavailable in sandbox — hard requirement not violated)
• TARGETS.md phase updated
• Memory updated
• 🔬 disclosure on all outputs

---

Warning

Protected Files — Push Permission Denied

This was originally intended as a pull request, but the patch modifies protected files. A human must create the pull request manually.

Protected files

• .github/workflows/lean-proofs.yml

The push was rejected because GitHub Actions does not have workflows permission to push these changes, and is never allowed to make such changes, or other authorization being used does not have this permission.

Create the pull request manually

# Download the patch from the workflow run
gh run download 25239813116 -n agent -D /tmp/agent-25239813116

# Create a new branch
git checkout -b lean-squad/task2-task9-arity-spec-ci-2026-05-02-ce2491bf50ed47e0 main

# Apply the patch (--3way handles cross-repo patches)
git am --3way /tmp/agent-25239813116/aw-lean-squad-task2-task9-arity-spec-ci-2026-05-02.patch

# Push the branch and create the pull request
git push origin lean-squad/task2-task9-arity-spec-ci-2026-05-02-ce2491bf50ed47e0
gh pr create --title '[Lean Squad] feat(fv): Task 2 + Task 9 — arity validator informal spec + sorry regression guard' --base main --head lean-squad/task2-task9-arity-spec-ci-2026-05-02-ce2491bf50ed47e0 --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.