[Lean Squad] feat(fv): Task 1 — expand TARGETS.md to 17 targets; add LLMEnvironmentDetector research by Evangelink · Pull Request #8115 · microsoft/testfx

Evangelink · 2026-05-11T13:50:58Z

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

…tDetector research - 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>

Copilot

Pull request overview

Updates the Lean Squad formal-verification documentation to reflect the expanded set of tracked FV targets (now 17) and adds research notes for a newly identified target around LLMEnvironmentDetector rule composition.

Changes:

Expanded formal-verification/TARGETS.md with a consolidated 17-target table, updated priority order, and a new findings section (BUG/OQ/GAP items).
Added a new Target 17 research section describing LLMEnvironmentDetector rule composition goals and proposed Lean modelling approach.
Added a corresponding Target 17 research entry to formal-verification/RESEARCH.md.

Show a summary per file

File	Description
formal-verification/TARGETS.md	Reworks the targets list and adds findings + new Target 17 research summary.
formal-verification/RESEARCH.md	Adds a detailed research subsection for Target 17 (`LLMEnvironmentDetector`).

Copilot's findings

Files reviewed: 2/2 changed files
Comments generated: 3

+This recently-added helper detects whether the current process is running inside an LLM-powered coding agent (Claude Code, Copilot, Cursor, Gemini, etc.). It models detection as a composition of three primitive rule types:
+
+- `BooleanEnvironmentRule`: any env var ∈ list parses as `true` (via `ParseBool`)
+- `AnyPresentEnvironmentRule`: any env var ∈ list is non-null/non-empty
+- `AnyPresentEnvironmentRule`: env var has a specific value (case-insensitive)


+
+- `BooleanEnvironmentRule`: any env var ∈ list parses as `true` (via `ParseBool`)
+- `AnyPresentEnvironmentRule`: any env var ∈ list is non-null/non-empty
+- `AnyPresentEnvironmentRule`: env var has a specific value (case-insensitive)


+5. `ParseBool("1", _)` = `true`, `ParseBool("0", _)` = `false` (decidable)
+6. `ParseBool` result ∈ {`true`, `false`} for any input (trivially true)
+
+**Approximations**: Model environment as a `HashMap String (Option String)`. The `AnyMatchEnvironmentRule` list is modelled as a `List Rule`.


Evangelink

Summary

Workflow: PR Nitpick Reviewer
Date: 2026-05-11
Repository: microsoft/testfx

Key Findings

This PR expands TARGETS.md from 8 to 17 formal-verification targets and adds a research entry for LLMEnvironmentDetector in RESEARCH.md. The changes are well-structured, but there are a few internal consistency issues introduced between the two new Target 17 sections:

Important — Duplicate rule type label (TARGETS.md line 75): The third bullet in the rule-type list repeats AnyPresentEnvironmentRule instead of EnvironmentVariableValueRule, which is the actual class name in the source.
Important — Incorrect rule count (TARGETS.md line 71): The text says "three primitive rule types" but four are enumerated; RESEARCH.md correctly says "four rule types".
Minor — Stale target count in Notes (TARGETS.md line 100): "Fourteen targets" should now read "Seventeen" after this PR's additions.
Minor — Imprecise "inside this file" reference (RESEARCH.md line 214): EnvironmentVariableParser.ParseBool is in EnvironmentVariableParser.cs, not LLMEnvironmentDetector.cs — a fact this same PR already corrects in the TARGETS table for id=8.

Positive Highlights

Excellent addition of the Findings table — centralising BUG-N/OQ-N findings in one place makes it much easier to track which targets have confirmed defects.
The new targets (9–17) are consistently formatted and include useful Notes column entries.
Cross-referencing between the RESEARCH.md entry and the TARGETS.md table via id= identifiers is a clean convention.

Recommendations

Fix the four consistency issues noted above before merging to keep the FV documentation trustworthy as a reference for future Lean modelling work.

Generated by PR Nitpick Reviewer

🔍 Meticulously inspected by PR Nitpick Reviewer 🔍

Evangelink · 2026-05-11T13:55:51Z

+- `AnyMatchEnvironmentRule []` → always `false` (empty OR = false identity)
+- `AnyMatchEnvironmentRule [r]` is extensionally equal to `r.IsMatch()` (singleton identity)
+- Monotonicity: adding a rule can only increase detection (inductive)
+- `EnvironmentVariableParser.ParseBool` inside this file is the same logic as target id=8 — the Lean model can be reused


Nitpick (Minor): "inside this file" is misleading. The target file being described is LLMEnvironmentDetector.cs, but EnvironmentVariableParser.ParseBool lives in the separate file EnvironmentVariableParser.cs (as correctly reflected by target id=8 in TARGETS.md which was updated in this same PR). Consider replacing "inside this file" with "defined in EnvironmentVariableParser.cs" to be precise.

Why it matters: A reader trying to locate the logic to model in Lean might look in the wrong file.

Evangelink · 2026-05-11T13:55:51Z

+
+- `BooleanEnvironmentRule`: any env var ∈ list parses as `true` (via `ParseBool`)
+- `AnyPresentEnvironmentRule`: any env var ∈ list is non-null/non-empty
+- `AnyPresentEnvironmentRule`: env var has a specific value (case-insensitive)


Nitpick (Important): This bullet is a duplicate label — it says AnyPresentEnvironmentRule again, but the actual class at this position is EnvironmentVariableValueRule (confirmed in LLMEnvironmentDetector.cs line 149). Both this entry and the one on the preceding line currently read AnyPresentEnvironmentRule, which makes the list incorrect and confusing.

Suggested correction:

- `EnvironmentVariableValueRule`: env var has a specific value (case-insensitive)

Why it matters: The rule taxonomy is the core of this FV target's description; a mis-labelled rule type will cause confusion when someone tries to model these rules in Lean.

Evangelink · 2026-05-11T13:55:51Z

- MSTest assertion APIs (e.g., `Assert.AreEqual`, `Assert.IsTrue`) remain interesting but harder to model formally due to generic type constraints and exception-based control flow.
- Future targets may include the server-mode protocol state machine and the test-filter tokeniser (`TreeNodeFilter.TokenizeFilter`).
+- Lean 4 toolchain installation has been blocked in the agent sandbox for 14 consecutive runs (elan binary execution denied by security policy). All Tasks 3–5 are deferred until this is resolved.
+- Fourteen targets are in Microsoft.Testing.Platform (command-line infrastructure, server mode, helpers). One target (`UnitTestOutcomeHelper` gaps) is in the MSTest adapter.


Nitpick (Minor): "Fourteen targets are in Microsoft.Testing.Platform" is stale after this PR expands the list to 17 targets (all of which have file paths under src/Platform/Microsoft.Testing.Platform/). Consider updating to "Seventeen targets".

Why it matters: Stale counts in a tracking document erode trust in the document's accuracy.

Evangelink · 2026-05-11T13:55:51Z

+**File**: `src/Platform/Microsoft.Testing.Platform/Helpers/LLMEnvironmentDetector.cs`
+**Type**: Internal rule-based DSL for AI-tool environment detection
+
+This recently-added helper detects whether the current process is running inside an LLM-powered coding agent (Claude Code, Copilot, Cursor, Gemini, etc.). It models detection as a composition of three primitive rule types:


Nitpick (Important): Says "three primitive rule types" but then lists four (BooleanEnvironmentRule, AnyPresentEnvironmentRule, EnvironmentVariableValueRule, AnyMatchEnvironmentRule). The corresponding entry in RESEARCH.md correctly says "four rule types". The count here should be updated to match.

Why it matters: The number directly contradicts the list that follows, and creates an inconsistency between the two documents in the same PR.

…LLMEnvironmentDetector research (#8115) Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot AI review requested due to automatic review settings May 11, 2026 13:50

Evangelink merged commit 7c3244b into main May 11, 2026
15 of 16 checks passed

Evangelink deleted the lean-squad/run14-task1-targets-update-2026-05-11-5dc032362e20517c branch May 11, 2026 13:51

Copilot started reviewing on behalf of Evangelink May 11, 2026 13:51 View session

Copilot AI reviewed May 11, 2026

View reviewed changes

Evangelink commented May 11, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

[Lean Squad] feat(fv): Task 1 — expand TARGETS.md to 17 targets; add LLMEnvironmentDetector research#8115
Evangelink merged 1 commit into
mainfrom
lean-squad/run14-task1-targets-update-2026-05-11-5dc032362e20517c

Evangelink commented May 11, 2026

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Evangelink left a comment

Uh oh!

Evangelink May 11, 2026

Uh oh!

Evangelink May 11, 2026

Uh oh!

Evangelink May 11, 2026

Uh oh!

Evangelink May 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

Evangelink commented May 11, 2026

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Copilot's findings

Uh oh!

Evangelink left a comment

Choose a reason for hiding this comment

Summary

Key Findings

Positive Highlights

Recommendations

Uh oh!

Evangelink May 11, 2026

Choose a reason for hiding this comment

Uh oh!

Evangelink May 11, 2026

Choose a reason for hiding this comment

Uh oh!

Evangelink May 11, 2026

Choose a reason for hiding this comment

Uh oh!

Evangelink May 11, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants