[Lean Squad] feat(fv): Task 1 — expand TARGETS.md to 17 targets; add LLMEnvironmentDetector research

[Evangelink]

🔬 Lean Squad — Formal Verification PR

This PR was created by the Lean Squad automated FV agent. Run: 25645127282

---

What's in this PR

Task 1 — Research & Target Identification (run 14)

This PR brings formal-verification/TARGETS.md up to date with all 17 tracked FV targets accumulated over 14 agent runs, replacing the outdated 7-entry version on main.

Changes

formal-verification/TARGETS.md — complete rewrite:

• Expanded from 7 → 17 entries
• All targets from agent memory (runs 1–13) consolidated into a clean table
• Added findings table (BUG-1..BUG-5, OQ-1..OQ-4, GAP-1..GAP-2)
• Added consolidated priority order with rationale
• Added new target 17: LLMEnvironmentDetector rule composition (identified this run)
• Noted 14-run Lean toolchain block in Notes section

formal-verification/RESEARCH.md — new section added:

• Full research notes for Target 17 — LLMEnvironmentDetector rule composition
• Pure rule-based DSL for AI coding-tool detection (Claude Code, Copilot, Cursor, Gemini, etc.)
• Composition laws: empty-OR=false identity, singleton identity, monotonicity
• ParseBool inside it reuses the same logic as tracked target id=8

New Target 17 — LLMEnvironmentDetector

File: src/Platform/Microsoft.Testing.Platform/Helpers/LLMEnvironmentDetector.cs
Rule types: BooleanEnvironmentRule, AnyPresentEnvironmentRule,
            EnvironmentVariableValueRule, AnyMatchEnvironmentRule

Properties to verify (all decidable or inductively provable):
1. AnyMatchEnvironmentRule [] → always false (empty OR = false)
2. AnyMatchEnvironmentRule [r] = r.IsMatch()
3. Monotonicity: adding a rule can only increase detection
4. ParseBool null default = default
5. ParseBool "1" _ = true, ParseBool "0" _ = false

Lean Toolchain Status

⚠️ LEAN_AVAILABLE=false — Lean 4 toolchain (elan) installation is blocked by the agent's security policy (execution denied). This is the 14th consecutive run where Lean cannot be run. Tasks 3–5 remain deferred.

No .lean files are included in this PR (hard requirement: no unverified Lean code).

---

Supersedes

This PR consolidates changes from several earlier open PRs that updated TARGETS.md:

• [Lean Squad] feat(fv): Task 1 — add 3 new FV targets and sync TARGETS.md phases #8042, [Lean Squad] feat(fv): Task 1 — add 3 new FV targets (PasteArguments, TimeSpanParser, TokenizeFilter) #8037, [Lean Squad] feat(fv): Task 1 — add 3 new FV targets and sync TARGETS.md phases #8017, [Lean Squad] feat(fv): Task 1 — add 3 new FV targets (UnicodeCharacterUtilities, TestNodeUid, CommandLineOption) #8014, [Lean Squad] feat(fv): Task 1 — add 5 new FV targets (PasteArguments, TimeSpanParser, TokenizeFilter, Sha256Hasher, ExtensionValidationHelper [Content truncated due to length] #8004, [Lean Squad] feat(fv): Task 1 — expand FV targets to 10 (TokenizeFilter, OptionName, GetElementCounts) #7991, [Lean Squad] feat(fv): Task 1 — add 3 new FV targets (PasteArguments, TimeSpanParser, TokenizeFilter) #7996, [Lean Squad] feat(fv): Task 1 — expand FV targets from 7 to 14 with detailed research #8076 (all updating TARGETS.md with 8-14 targets)

Once this PR is merged, those PRs can be closed as superseded.

---

🔬 This PR was generated automatically by the Lean Squad FV agent.

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 25645127282 -n agent -D /tmp/agent-25645127282

# Create a new branch
git checkout -b lean-squad/run14-task1-targets-update-2026-05-11-5dc032362e20517c

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25645127282/aw-lean-squad-run14-task1-targets-update-2026-05-11.patch

# Push the branch to origin
git push origin lean-squad/run14-task1-targets-update-2026-05-11-5dc032362e20517c

# Create the pull request
gh pr create --title '[Lean Squad] feat(fv): Task 1 — expand TARGETS.md to 17 targets; add LLMEnvironmentDetector research' --base main --head lean-squad/run14-task1-targets-update-2026-05-11-5dc032362e20517c --repo microsoft/testfx

Show patch preview (195 of 195 lines)

From 2e5dd7ed74ac8e83bdf687d0064a2680b89449c2 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Mon, 11 May 2026 01:18:43 +0000
Subject: [PATCH] =?UTF-8?q?feat(fv):=20Task=201=20=E2=80=94=20expand=20TAR?=
 =?UTF-8?q?GETS.md=20to=2017=20targets;=20add=20LLMEnvironmentDetector=20r?=
 =?UTF-8?q?esearch?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Updated TARGETS.md from 7 to 17 entries (reflects 14 runs of accumulated memory)
- Added all previously-tracked targets (ids 1-16) in a consolidated clean table
- Added new target 17: LLMEnvironmentDetector rule composition
  - Rule-based DSL for AI coding-tool detection (pure, algebraic)
  - Composition laws: empty OR=false, singleton identity, monotonicity
  - ParseBool logic reuses same Lean model as target id=8
- Updated findings table (BUG-1..BUG-5, OQ-1..OQ-4, GAP-1..GAP-2)
- Added new target section to RESEARCH.md with full rationale
- Task 3 remains blocked: Lean toolchain (elan) execution denied by
  agent security policy (confirmed 14 consecutive runs)

🔬 Lean Squad automated FV agent — run 25645127282

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

diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
index 64975c761..01b5a650e 100644
--- a/formal-verification/RESEARCH.md
+++ b/formal-verification/RESEARCH.md
@@ -193,6 +193,41 @@ A pure recursive function that evaluates whether a test-node path and property b
 
 ---
 
+### Target 17 — `LLMEnvironmentDetector` rule composition ★★★☆☆
+
+**File**: `src/Platform/Microsoft.Testing.Platform/Helpers/LLMEnvironmentDetector.cs`
+**Type**: Internal rule-based DSL for AI coding-tool detection
+
+This recently-added helper detects whether the proces
... (truncated)