[Lean Squad] feat(fv): Task 1 — add 3 new FV targets and sync TARGETS.md phases

[Evangelink]

🔬 Lean Squad — automated formal verification agent run (workflow run)

---

What

This PR (Task 1 — Research & Target Identification) makes two improvements to the FV target registry:

1. Sync TARGETS.md with actual phase state

TARGETS.md had drifted from the agent's memory — several targets showed phase 1 when informal specs had already been extracted (phase 2), and targets 8–10 from prior runs were missing entirely.

Fixed phases:

#	Target	Was	Now
3	CommandLineParser.ParseOptionAndSeparators	— (missing)	phase 2 + PR link
4	ValidateOptionsArgumentArity	phase 1	phase 2
5	CommandLineParseResult.Equals	phase 1	phase 2 + PR link
7	TreeNodeFilter.MatchFilterPattern	— (missing)	phase 2 + PR link
8–10	PasteArguments, TimeSpanParser, TokenizeFilter	— (missing)	phase 1, identified

2. Add 3 new targets from previously unexplored areas

#	Target	File	Why
11	ValidationResult struct	Extensions/ValidationResult.cs	Invariant: IsValid ↔ ErrorMessage = none; all 5 theorems are decide-provable. Cleanest possible Task-3 warm-up.
12	ExitCode enum	Helpers/ExitCodes.cs	Source doc comment requires POSIX range [0, 255]; distinctness + range fully decide-provable.
13	TestNodePropertiesCategories	Messages/TestNodeProperties.Categories.cs	FailedProperties ⊆ OutcomeProperties is an implicit invariant not enforced by the type system; a single decide proof guards it.

Detailed write-ups for all three targets have been appended to RESEARCH.md.

Why these targets

• Target 11 (ValidationResult) is the cleanest next Task 3 candidate once the Lean toolchain becomes available. Two fields, two factory methods, one invariant.
• Target 12 (ExitCode) makes the documented POSIX constraint machine-checked. If a developer adds a new code > 255, the proof will fail.
• Target 13 (TestNodePropertiesCategories) guards a safety-critical array-subset relationship that the type system cannot express.

Notes

• Lean toolchain is still unavailable in the sandbox (network-blocked elan). Task 3 remains unblocked on the CI side.
• No .lean files are modified in this PR.

Generated by 📐 Lean Squad, see workflow run.

---

Note

This was originally intended as a pull request, but the git push operation failed.

Workflow Run: View run details and download patch artifact

The patch file is available in the agent artifact in the workflow run linked above.

To create a pull request with the changes:

# Download the artifact from the workflow run
gh run download 25426022813 -n agent -D /tmp/agent-25426022813

# Create a new branch
git checkout -b lean-squad/task1-new-targets-2026-05-06-run2-3dd3e2a126b8a28d

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25426022813/aw-lean-squad-task1-new-targets-2026-05-06-run2.patch

# Push the branch to origin
git push origin lean-squad/task1-new-targets-2026-05-06-run2-3dd3e2a126b8a28d

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 1 — add 3 new FV targets and sync TARGETS.md phases' --base main --head lean-squad/task1-new-targets-2026-05-06-run2-3dd3e2a126b8a28d --repo microsoft/testfx

Show patch preview (239 of 239 lines)

From 26b0d5021906b0bb2fd10be3911c0dfdc5bfd68a Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Wed, 6 May 2026 09:19:08 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=201=20=E2=80=94=20add=203=20ne?=
 =?UTF-8?q?w=20FV=20targets=20and=20sync=20TARGETS.md=20to=20phase=202?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Sync all target phases in TARGETS.md with current state (targets 3–7
  were at phase 2 but shown as phase 1 or missing from the table)
- Add targets 8–10 (PasteArguments, TimeSpanParser, TokenizeFilter)
  which were identified in prior runs but missing from TARGETS.md
- Add 3 new targets from previously unexplored areas:
    - Target 11: ValidationResult struct (Extensions namespace)
      Invariant: IsValid ↔ ErrorMessage = none; all decide-provable
    - Target 12: ExitCode enum (Helpers namespace)
      POSIX range constraint [0,255]; pairwise distinctness; decide-provable
    - Target 13: TestNodePropertiesCategories subset invariant (Messages)
      FailedProperties ⊆ OutcomeProperties; disjointness with Discovered
- Update priority ordering to reflect the new target set
- Append detailed target write-ups for targets 11–13 to RESEARCH.md

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 formal-verification/RESEARCH.md |  72 ++++++++++++++++++++++
 formal-verification/TARGETS.md  | 102 ++++++++++++++++++++++++++++----
 2 files changed, 164 insertions(+), 10 deletions(-)

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..2e468560c 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -193,6 +193,78 @@ A pure recursive function that evaluates whether a test-node path and property b
 
 ---
 
+---
+
+### Target 11 — `ValidationResult` struct — Complementary Validity Invariant ★★★★★
+
+**File**: `src/Platform/Microsoft.Testing.Platform/Extensions/V
... (truncated)

[Evangelink]

Closing — the Lean formal verification workflow is being removed in #8121.