[Lean Squad] feat: formal verification infrastructure — research & CI automation

.github/workflows/lean-proofs.yml

@@ -0,0 +1,77 @@
+name: Lean Proofs
+
+# 🔬 Lean Squad — CI workflow for formal verification proofs.
+# Runs `lake build` to verify Lean 4 proofs in formal-verification/lean/.
+
+permissions:
+  contents: read
+
+on:
+  pull_request:
+    paths:
+      - "formal-verification/lean/**"
+      - ".github/workflows/lean-proofs.yml"
+  push:
+    branches:
+      - main
+    paths:
+      - "formal-verification/lean/**"
+  workflow_dispatch:
+
+jobs:
+  lean-build:
+    name: Build Lean proofs
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install elan (Lean version manager)
+        run: |
+          ELAN_VERSION="v4.2.1"
+          ELAN_TARGET="x86_64-unknown-linux-gnu"
+          ELAN_ARCHIVE="elan-${ELAN_TARGET}.tar.gz"
+          ELAN_BASE_URL="https://github.com/leanprover/elan/releases/download/${ELAN_VERSION}"
+          ELAN_TMP_DIR="$(mktemp -d)"
+
+          LEAN_TOOLCHAIN_FILE="formal-verification/lean/lean-toolchain"
+
+          if [ ! -f "${LEAN_TOOLCHAIN_FILE}" ]; then
+            echo "Missing Lean toolchain file: ${LEAN_TOOLCHAIN_FILE}" >&2
+            exit 1
+          fi
+
+          LEAN_TOOLCHAIN="$(tr -d '\r\n' < "${LEAN_TOOLCHAIN_FILE}")"
+
+          if [ -z "${LEAN_TOOLCHAIN}" ]; then
+            echo "Lean toolchain file is empty: ${LEAN_TOOLCHAIN_FILE}" >&2
+            exit 1
+          fi
+
+          curl -sSfL "${ELAN_BASE_URL}/${ELAN_ARCHIVE}" -o "${ELAN_TMP_DIR}/${ELAN_ARCHIVE}"
+          cd "${ELAN_TMP_DIR}"
+          echo "4e717523217af592fa2d7b9c479410a31816c065d66ccbf0c2149337cfec0f5c  ${ELAN_ARCHIVE}" | sha256sum -c -
+          tar -xzf "${ELAN_ARCHIVE}"
+          ./elan-init -y --default-toolchain "${LEAN_TOOLCHAIN}"
+          rm -rf "${ELAN_TMP_DIR}"
+
+      - name: Add elan to PATH
+        run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Show Lean version
+        run: lean --version
+
+      - name: Cache Lean / Lake build artifacts
+        uses: actions/cache@v4
+        with:
+          path: |
+            formal-verification/lean/.lake
+            ~/.elan
+          key: lean-${{ runner.os }}-${{ hashFiles('formal-verification/lean/lakefile.toml', 'formal-verification/lean/lake-manifest.json') }}
+          restore-keys: |
+            lean-${{ runner.os }}-
+
+      - name: Build Lean proofs
+        working-directory: formal-verification/lean
+        run: lake build

.gitignore

@@ -88,6 +88,9 @@ ehthumbs.db
 /.dotnet/
 /TestAssets/
 
+# Lean build artifacts
+.lake/
+
 # ===========================
 # Tools
 # ===========================

.markdownlint-cli2.jsonc

@@ -149,6 +149,7 @@
     "artifacts/tmp/**/*.md",
     "eng/**/*.md",
     "tools/**/*.md",
+    "formal-verification/**/*.md",
     ".dotnet/**/*.md",
     ".github/ISSUE_TEMPLATE/**/*.md",
     ".github/skills/**/*.md",

azure-pipelines-official.yml

@@ -11,6 +11,7 @@ trigger:
     exclude:
       - .github/**
       - .gitignore
+      - formal-verification/**
 
 parameters:
 - name: isRTM

azure-pipelines.yml

@@ -7,6 +7,7 @@ trigger:
     exclude:
       - .github/**
       - .gitignore
+      - formal-verification/**
 
 # Branch(es) that trigger(s) build(s) on PR
 pr:
@@ -17,6 +18,7 @@ pr:
     exclude:
       - .github/**
       - .gitignore
+      - formal-verification/**
       - .devcontainer/*
       - docs/*
       - .vscode/*

formal-verification/CORRESPONDENCE.md

@@ -0,0 +1,7 @@
+# Lean–C# Correspondence
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+This document records how each Lean 4 model corresponds to the C# source it is meant to represent, including deliberate approximations and abstractions.
+
+_No targets have reached Phase 4 (implementation extraction) yet. This document will be populated as targets advance._

formal-verification/CRITIQUE.md

@@ -0,0 +1,7 @@
+# FV Critique
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+This document records an ongoing assessment of the utility and coverage of the formal verification work in this repository.
+
+_No targets have been proved yet. Critique will be added as proofs are completed._

formal-verification/REPORT.md

@@ -0,0 +1,35 @@
+# FV Project Report
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+## Status
+
+**Phase**: Early — Research complete, informal spec for `ArgumentArity` extracted.
+
+## Summary
+
+The Lean Squad has surveyed the `microsoft/testfx` codebase and identified five high-quality FV targets in the command-line infrastructure of Microsoft.Testing.Platform. All five targets are pure or near-pure functions with clear algebraic properties, making them suitable for Lean 4 formal verification.
+
+An informal specification has been extracted for `ArgumentArity` (highest-priority target): 14 properties across four groups (predefined constants, well-formedness, equality, distinctness). One open question identified: the constructor does not enforce `Min ≤ Max`, so ill-formed arities are silently accepted. This is a potential source of undefined validator behavior.
+
+The next steps are:
+1. Write the Lean 4 formal spec for `ArgumentArity` (types + theorem stubs).
+2. Attempt decidable proofs with `decide`.
+3. Advance to `CommandLineParser.TryUnescape`.
+
+## Targets Identified
+
+| Target | Phase | Notes |
+|--------|-------|-------|
+| `ArgumentArity` | 2 | Informal spec extracted — 14 properties, open question on ill-formed arity |
+| `CommandLineParser.TryUnescape` | 1 | Security-relevant string unescaping |
+| `CommandLineParser.ParseOptionAndSeparators` | 1 | Pure option-splitting function |
+| `CommandLineOptionsValidator` arity validation | 1 | Arity bounds checking |
+| `CommandLineParseResult.Equals` | 1 | Structural equality laws |
+
+## Run History
+
+| Date | Tasks | Outcome |
+|------|-------|---------|
+| 2026-04-24 | Task 1 (Research), Task 2 (Informal Spec), Task 9 (CI Automation) | Identified 5 targets; extracted informal spec for ArgumentArity (14 properties, open question on ill-formed arity); set up CI workflow |
+| 2026-04-24 | Task 1 (Research), Task 9 (CI Automation) | Identified targets, created FV directory, set up CI workflow |

formal-verification/RESEARCH.md

@@ -0,0 +1,155 @@
+# Formal Verification Research
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+## Repository Overview
+
+**Repository**: `microsoft/testfx`
+**Primary Language**: C# (.NET)
+**Codebase Components**:
+- **MSTest** (`src/TestFramework/`): The MSTest v3 testing framework for .NET — assertion APIs, test attributes, data-driven tests.
+- **Microsoft.Testing.Platform** (`src/Platform/Microsoft.Testing.Platform/`): A modern, extensible test runner platform — command-line parsing, server mode, extensions.
+- **Adapters and Extensions** (`src/Adapter/`, `src/Platform/Microsoft.Testing.Extensions.*/`): VSTest bridge, telemetry, coverage, retry, crash dump, etc.
+- **Analyzers** (`src/Analyzers/`): Roslyn-based diagnostic analyzers for MSTest usage.
+
+## FV Tool Choice
+
+**Lean 4** with **Mathlib** (standard Lean 4 library for mathematics and formal proofs).
+
+**Rationale**:
+- Lean 4 has excellent decidable-proposition support (`decide` tactic).
+- Mathlib provides rich libraries for lists, strings, and algebraic structures.
+- Lean 4's dependent type system allows encoding invariants as types.
+- Active ecosystem with CI integration via `lake build`.
+
+## FV Strategy
+
+This project applies formal verification **incrementally**, one target at a time:
+
+1. Identify **pure or near-pure functions** with clear algebraic properties.
+2. Write **informal specs** capturing intent from code, tests, and documentation.
+3. Translate to **Lean 4 type definitions and theorem statements** (with `sorry`).
+4. **Attempt proofs** using `decide`, `omega`, `simp`, `induction`, etc.
+5. Report **bugs** when a proposition cannot be proved and the spec is correct.
+
+We focus on **structural properties** and **invariants** rather than full functional equivalence (which would require modelling all of .NET's runtime semantics).
+
+## Identified FV-Amenable Targets
+
+### Target 1 — `ArgumentArity` ★★★★★
+
+**File**: `src/Platform/Microsoft.Testing.Extensions.CommandLine/ArgumentArity.cs`
+**Type**: `readonly struct ArgumentArity(int min, int max)`
+
+A simple value struct for describing how many arguments a command-line option accepts.
+
+**Why ideal for FV**:
+- Tiny, self-contained type with only two integer fields.
+- Five predefined constants with documented semantics.
+- `IEquatable<T>` implementation to verify.
+- Invariant: for all well-formed arities, `Min ≤ Max` — **not enforced by the constructor**.
+- Equality properties (reflexivity, symmetry, transitivity) are easily decidable.
+
+**Properties to verify**:
+1. All five predefined constants satisfy `Min ≤ Max`.
+2. `Zero` has Min=0, Max=0.
+3. `ZeroOrOne` has Min=0, Max=1.
+4. `ZeroOrMore` has Min=0, Max=`maxInt32`.
+5. `OneOrMore` has Min=1, Max=`maxInt32`.
+6. `ExactlyOne` has Min=1, Max=1.
+7. `Equals` is an equivalence relation (reflexive, symmetric, transitive).
+8. `==` and `!=` agree with `Equals`.
+
+**Approximations**: Model `int.MaxValue` with an explicit Lean sentinel constant, for example `def maxInt32 : Int := 2^31 - 1`.
+
+---
+
+### Target 2 — `CommandLineParser.TryUnescape` ★★★★☆
+
+**File**: `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` (inner function)
+**Informal signature**: command-line text × optional quote context × environment → either unescaped text or an error message
+
+A pure function that unescapes command-line argument strings — handling single-quote and double-quote conventions.
+
+**Why good for FV**:
+- Pure (no side effects, no I/O).
+- Well-documented convention via comments in source.
+- Clear case analysis: plain string / single-quoted / double-quoted.
+
+**Properties to verify**:
+1. Single-quoted strings without interior quotes → strip outer quotes.
+2. Single-quoted strings with interior quotes → error.
+3. Double-quoted strings → strip quotes and apply backslash-escape rules.
+4. Unquoted strings → returned unchanged.
+5. Result of successful unescaping never starts or ends with the outer quote character.
+
+**Approximations**: Lean model abstracts `IEnvironment.NewLine` as a parameter; does not model environment variable expansion.
+
+---
+
+### Target 3 — `CommandLineParser.ParseOptionAndSeparators` ★★★★☆
+
+**File**: `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` (inner function)
+**Type**: `string → string × option(string)`
+
+Splits a raw argument like `--option=value` or `--option:value` or `--option` into option name and argument.
+
+**Properties to verify**:
+1. If the input contains no `:` or `=`, the result argument is `none`.
+2. If the input contains `:` or `=`, the option name is `input[..delimiterIndex]` and argument is the rest.
+3. The returned option name has all leading `-` characters stripped.
+4. If the delimiter is the first character, the option name is empty string.
+
+**Approximations**: Models `IndexOfAny` over two characters; string indexing.
+
+---
+
+### Target 4 — `CommandLineOptionsValidator` arity validation ★★★☆☆
+
+**File**: `src/Platform/Microsoft.Testing.Platform/CommandLine/CommandLineOptionsValidator.cs`
+**Function**: `ValidateOptionsArgumentArity`
+
+Checks that each parsed option has an argument count within its registered arity bounds.
+
+**Properties to verify**:
+1. If an option has `Max=0` and `argumentCount > 0` → error.
+2. If `argumentCount < Min` → error.
+3. If `argumentCount > Max` (and `Max > 0`) → error.
+4. If `Min ≤ argumentCount ≤ Max` → no error for that option.
+5. An option with `Arity = Zero` and zero arguments produces no error.
+
+**Approximations**: Must model a simplified option registry; abstracts over provider identity.
+
+---
+
+### Target 5 — `CommandLineParseResult` structural equality ★★★☆☆
+
+**File**: `src/Platform/Microsoft.Testing.Platform/CommandLine/ParseResult.cs`
+**Function**: `Equals(CommandLineParseResult?)`
+
+Structural equality over a parse result: tool name, list of options (name + argument list), and list of errors.
+
+**Properties to verify**:
+1. Reflexivity: `r.Equals(r)` is always true.
+2. Symmetry: `r1.Equals(r2) ↔ r2.Equals(r1)`.
+3. Transitivity: `r1.Equals(r2) ∧ r2.Equals(r3) → r1.Equals(r3)`.
+4. Empty parse result equals itself.
+5. Two results differing only in tool name are not equal.
+
+**Approximations**: Model strings as `String` (Lean), argument lists as `List String`.
+
+---
+
+## Approach Notes
+
+- We use Lean 4 with Mathlib for all proofs.
+- We translate C# business logic into **pure functional Lean models**, explicitly noting what is abstracted away.
+- `sorry` is used liberally early on; the goal is to get theorems stated correctly, then fill proofs.
+- For simple finite types (like `ArgumentArity` constants), we rely on `decide` for closed proofs.
+- We track which theorems are `sorry`-guarded vs. fully proved in `TARGETS.md`.
+
+## Open Questions
+
+- Should we model `int.MaxValue` as an explicit Lean constant (e.g., `def maxInt32 : Int := 2^31 - 1`) or leave it as an opaque constant?
+- The `TryUnescape` function handles environment `NewLine` — should we abstract over this or assume `"\n"`?
+- Is the lack of a `Min ≤ Max` invariant in `ArgumentArity` a real bug or an accepted API choice? Worth filing an issue if a "bad" arity causes unexpected validator behaviour.

formal-verification/TARGETS.md

@@ -0,0 +1,38 @@
+# FV Targets
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+## Legend
+
+| Phase | Description |
+|-------|-------------|
+| 1 | Research — identified, rationale documented |
+| 2 | Informal spec extracted |
+| 3 | Lean 4 formal spec written (type signatures + theorem stubs) |
+| 4 | Lean 4 implementation model extracted |
+| 5 | Proofs attempted / completed |
+
+## Target List
+
+| # | Name | File | Phase | Status | PR/Issue |
+|---|------|------|-------|--------|----------|
+| 1 | `ArgumentArity` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ArgumentArity.cs` | 2 | Informal spec extracted | [PR #7799](https://github.com/microsoft/testfx/pull/7799) |
+| 2 | `CommandLineParser.TryUnescape` | `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` | 1 | Identified | — |
+| 3 | `CommandLineParser.ParseOptionAndSeparators` | `src/Platform/Microsoft.Testing.Platform/CommandLine/Parser.cs` | 1 | Identified | — |
+| 4 | `CommandLineOptionsValidator` arity validation | `src/Platform/Microsoft.Testing.Platform/CommandLine/CommandLineOptionsValidator.cs` | 1 | Identified | — |
+| 5 | `CommandLineParseResult.Equals` | `src/Platform/Microsoft.Testing.Platform/CommandLine/ParseResult.cs` | 1 | Identified | — |
+
+## Priority Order
+
+1. **`ArgumentArity`** — highest priority. Smallest self-contained target; decidable properties; good warm-up for setting up the Lean environment.
+2. **`CommandLineParser.TryUnescape`** — second priority. Pure function with clear specification; security-relevant string processing.
+3. **`CommandLineParser.ParseOptionAndSeparators`** — third priority. Small pure function; useful for verifying parser correctness.
+4. **`CommandLineOptionsValidator` arity validation** — fourth priority. Validation logic with clear input/output contract.
+5. **`CommandLineParseResult.Equals`** — fifth priority. Structural equality; good for verifying equivalence-relation laws.
+
+## Notes
+
+- All five targets are in the command-line infrastructure (`src/Platform/Microsoft.Testing.Platform/CommandLine/`).
+- This focus makes sense: command-line parsing is pure and testable, with clear specification from the POSIX/CLI conventions.
+- MSTest assertion APIs (e.g., `Assert.AreEqual`, `Assert.IsTrue`) are interesting but harder to model formally due to generic type constraints and exception-based control flow.
+- Future targets may include the test-filter grammar and the server-mode protocol state machine.