diff --git a/.github/workflows/lean-proofs.yml b/.github/workflows/lean-proofs.yml
new file mode 100644
index 0000000000..f40c481715
--- /dev/null
+++ b/.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
diff --git a/.gitignore b/.gitignore
index 45021b9480..b20ce3e866 100644
--- a/.gitignore
+++ b/.gitignore
@@ -88,6 +88,9 @@ ehthumbs.db
 /.dotnet/
 /TestAssets/
 
+# Lean build artifacts
+.lake/
+
 # ===========================
 # Tools
 # ===========================
diff --git a/.markdownlint-cli2.jsonc b/.markdownlint-cli2.jsonc
index 4f80cdacf4..61de8f7a86 100644
--- a/.markdownlint-cli2.jsonc
+++ b/.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",
diff --git a/azure-pipelines-official.yml b/azure-pipelines-official.yml
index 1f8aa619c7..d63346bd2f 100644
--- a/azure-pipelines-official.yml
+++ b/azure-pipelines-official.yml
@@ -11,6 +11,7 @@ trigger:
     exclude:
       - .github/**
       - .gitignore
+      - formal-verification/**
 
 parameters:
 - name: isRTM
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 8cc6e62358..91f211a526 100644
--- a/azure-pipelines.yml
+++ b/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/*
diff --git a/formal-verification/CORRESPONDENCE.md b/formal-verification/CORRESPONDENCE.md
new file mode 100644
index 0000000000..3c74bc94c9
--- /dev/null
+++ b/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._
diff --git a/formal-verification/CRITIQUE.md b/formal-verification/CRITIQUE.md
new file mode 100644
index 0000000000..722a932e10
--- /dev/null
+++ b/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._
diff --git a/formal-verification/REPORT.md b/formal-verification/REPORT.md
new file mode 100644
index 0000000000..9628c77650
--- /dev/null
+++ b/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 |
diff --git a/formal-verification/RESEARCH.md b/formal-verification/RESEARCH.md
new file mode 100644
index 0000000000..8162919bcc
--- /dev/null
+++ b/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.
diff --git a/formal-verification/TARGETS.md b/formal-verification/TARGETS.md
new file mode 100644
index 0000000000..2e0fee3a89
--- /dev/null
+++ b/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.
diff --git a/formal-verification/lean/README.md b/formal-verification/lean/README.md
new file mode 100644
index 0000000000..8278dd9efb
--- /dev/null
+++ b/formal-verification/lean/README.md
@@ -0,0 +1,48 @@
+# Lean 4 Formal Verification — FVSquad
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+This directory contains the Lean 4 formal verification project for `microsoft/testfx`.
+
+## Structure
+
+```
+lean/
+  lakefile.toml          # Lake build configuration
+  FVSquad/
+    <Name>.lean          # One file per FV target (spec + implementation model + proofs)
+```
+
+## Building
+
+Requires [elan](https://github.com/leanprover/elan) (the Lean version manager).
+
+```bash
+# Install a pinned elan release (example for Linux x86_64)
+ELAN_VERSION=v4.2.1
+curl -sSfL -o elan.tar.gz "https://github.com/leanprover/elan/releases/download/${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz"
+curl -sSfL -o elan.tar.gz.sha256 "https://github.com/leanprover/elan/releases/download/${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz.sha256"
+sha256sum -c elan.tar.gz.sha256
+tar -xzf elan.tar.gz
+./elan-init -y
+
+# Build the project
+cd formal-verification/lean
+lake build
+```
+
+The `lean-toolchain` file pins the exact Lean version to match the Mathlib dependency.
+
+`lake build` creates a local `.lake/` directory with build artifacts.
+The repository root `.gitignore` ignores this directory to avoid accidentally committing
+generated files.
+
+## Status
+
+No Lean source files yet — targets are currently in Phase 1 (Research) or Phase 2 (Informal Spec).
+Lean source files will be added when targets advance to Phase 3 (Formal Spec Writing).
+
+## CI
+
+A GitHub Actions workflow (`.github/workflows/lean-proofs.yml`) runs `lake build`
+on every PR that modifies files in this directory.
diff --git a/formal-verification/lean/lakefile.toml b/formal-verification/lean/lakefile.toml
new file mode 100644
index 0000000000..3efa2eddcb
--- /dev/null
+++ b/formal-verification/lean/lakefile.toml
@@ -0,0 +1,11 @@
+name = "FVSquad"
+version = "0.1.0"
+defaultTargets = ["FVSquad"]
+
+[[lean_lib]]
+name = "FVSquad"
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.14.0"
diff --git a/formal-verification/lean/lean-toolchain b/formal-verification/lean/lean-toolchain
new file mode 100644
index 0000000000..1e70935f69
--- /dev/null
+++ b/formal-verification/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.14.0
diff --git a/formal-verification/specs/argument_arity_informal.md b/formal-verification/specs/argument_arity_informal.md
new file mode 100644
index 0000000000..e695fe4a60
--- /dev/null
+++ b/formal-verification/specs/argument_arity_informal.md
@@ -0,0 +1,134 @@
+# Informal Specification — `ArgumentArity`
+
+> 🔬 **Lean Squad** — auto-generated and maintained by the Lean Squad FV agent.
+
+## Target
+
+- **Type**: `readonly struct ArgumentArity(int min, int max)`
+- **Namespace**: `Microsoft.Testing.Platform.Extensions.CommandLine`
+- **File**: `src/Platform/Microsoft.Testing.Platform/CommandLine/ArgumentArity.cs`
+- **Phase**: 2 — Informal Spec
+- **Reference**: [System.CommandLine argument arity docs](https://learn.microsoft.com/dotnet/standard/commandline/syntax#argument-arity)
+
+---
+
+## Purpose
+
+`ArgumentArity` is a value type that describes the number of arguments a command-line option is allowed to accept. It stores a minimum (`Min`) and a maximum (`Max`) integer bound. The validator (`CommandLineOptionsValidator.ValidateOptionsArgumentArity`) uses these bounds to reject command-line invocations that provide too few or too many arguments for an option.
+
+---
+
+## Data Model
+
+```
+ArgumentArity = { Min : Int32, Max : Int32 }
+```
+
+There are five predefined named constants:
+
+| Name        | Min | Max            | Intended meaning              |
+|-------------|-----|----------------|-------------------------------|
+| `Zero`      | 0   | 0              | No arguments allowed          |
+| `ZeroOrOne` | 0   | 1              | Optional single argument      |
+| `ZeroOrMore`| 0   | `Int32.MaxValue`| Unlimited optional arguments |
+| `ExactlyOne`| 1   | 1              | Required single argument      |
+| `OneOrMore` | 1   | `Int32.MaxValue`| At least one argument        |
+
+`Int32.MaxValue` (2 147 483 647) is used as an "unbounded" sentinel.
+
+---
+
+## Preconditions
+
+- The struct has no validation in its constructor. Any combination of `min` and `max` is accepted, including negative values and `min > max`.
+- Well-formed arities satisfy `0 ≤ Min ≤ Max`. The five predefined constants all satisfy this.
+- The caller is responsible for providing well-formed arities; no exception is thrown for ill-formed ones.
+
+**Open question / potential bug**: if a caller creates `new ArgumentArity(5, 0)` (Min > Max), the validator produces inconsistent error messages. This is not currently caught.
+
+---
+
+## Postconditions / Properties
+
+### Property Group 1 — Predefined constants
+
+1. `Zero.Min == 0 ∧ Zero.Max == 0`
+2. `ZeroOrOne.Min == 0 ∧ ZeroOrOne.Max == 1`
+3. `ZeroOrMore.Min == 0 ∧ ZeroOrMore.Max == Int32.MaxValue`
+4. `ExactlyOne.Min == 1 ∧ ExactlyOne.Max == 1`
+5. `OneOrMore.Min == 1 ∧ OneOrMore.Max == Int32.MaxValue`
+
+### Property Group 2 — Well-formedness of predefined constants
+
+6. `∀ c ∈ {Zero, ZeroOrOne, ZeroOrMore, ExactlyOne, OneOrMore}, c.Min ≥ 0`
+7. `∀ c ∈ {Zero, ZeroOrOne, ZeroOrMore, ExactlyOne, OneOrMore}, c.Min ≤ c.Max`
+
+### Property Group 3 — Equality
+
+8. **Reflexivity**: `a.Equals(a) == true` for all `a`
+9. **Symmetry**: `a.Equals(b) == b.Equals(a)` for all `a, b`
+10. **Transitivity**: `a.Equals(b) ∧ b.Equals(c) → a.Equals(c)` for all `a, b, c`
+11. **Extensionality**: `a.Equals(b) ↔ (a.Min == b.Min ∧ a.Max == b.Max)`
+12. **Operator consistency**: `(a == b) ↔ a.Equals(b)` and `(a != b) ↔ !a.Equals(b)`
+13. `object.Equals` agrees with typed `Equals`: if `obj` is an `ArgumentArity`, then `a.Equals(obj) == a.Equals((ArgumentArity)obj)`
+
+### Property Group 4 — Distinctness of predefined constants
+
+14. All five predefined constants are pairwise distinct.
+   - `Zero ≠ ZeroOrOne ≠ ZeroOrMore ≠ ExactlyOne ≠ OneOrMore`
+   - (There are C(5,2) = 10 distinct pairs, all unequal.)
+
+---
+
+## Edge Cases
+
+- `new ArgumentArity(0, 0)` is definitionally equal to `Zero`.
+- `new ArgumentArity(1, Int32.MaxValue)` is definitionally equal to `OneOrMore`.
+- Negative `min` or `max` is accepted by the constructor but is not used by any predefined constant.
+- `min > max` is accepted by the constructor but creates an "impossible" arity that the validator would handle in an unspecified order.
+- `GetHashCode` is platform-conditional (`#if NET` uses `HashCode.Combine`; otherwise XOR). The equality contract requires that equal values have equal hash codes; this holds because `Equals` only checks `Min` and `Max`.
+
+---
+
+## Invariants
+
+1. The struct is immutable (`readonly`).
+2. Equality is defined structurally by `(Min, Max)` pair comparison.
+3. The predefined constants are `static readonly` fields — they are created once and shared.
+
+---
+
+## Examples
+
+| Expression | Result |
+|------------|--------|
+| `ArgumentArity.Zero.Equals(new ArgumentArity(0, 0))` | `true` |
+| `ArgumentArity.ExactlyOne == ArgumentArity.ZeroOrOne` | `false` |
+| `ArgumentArity.OneOrMore.Min` | `1` |
+| `ArgumentArity.ZeroOrMore.Max` | `2147483647` |
+| `new ArgumentArity(2, 5).Min ≤ new ArgumentArity(2, 5).Max` | `true` |
+| `new ArgumentArity(5, 0).Min ≤ new ArgumentArity(5, 0).Max` | `false` (ill-formed!) |
+
+---
+
+## Inferred Design Intent
+
+The design mirrors [System.CommandLine's `ArgumentArity`](https://learn.microsoft.com/dotnet/standard/commandline/syntax#argument-arity). The five constants cover the most common practical arity patterns. The struct is intentionally simple: no validation, no invariant enforcement, just a transparent (Min, Max) pair with structural equality. The burden of using well-formed arities lies with option providers.
+
+---
+
+## Open Questions for Lean Formalisation
+
+1. **Int32.MaxValue as sentinel**: Should we model `Int32.MaxValue` as Lean's `Int.ofNat (2^31 - 1)` (concrete) or as an opaque `unbounded` constant? The concrete approach allows `decide` to close proofs about predefined constants.
+2. **Ill-formed arities**: Should the Lean model admit ill-formed arities (Min > Max) or restrict to a subtype `{ a : ArgumentArity // a.Min ≤ a.Max }`? The subtype approach makes well-formedness part of the proof structure.
+3. **GetHashCode**: The hash code is platform-conditional. Should we model it? Probably not — it is not observable in the properties we want to verify.
+4. **`object.Equals` overload**: Should we verify the `bool Equals(object?)` overload? Yes — it adds a type-erasure property: `a.Equals((object)a)` is always true.
+
+---
+
+## Approximations for Lean Model
+
+- Model `int` as `Int` (unbounded integers) or `UInt32` or `Int32` (32-bit signed). For the predefined constants, `UInt32` suffices; for the general case, we need to handle negative values if we want to model ill-formed arities.
+- Do NOT model `GetHashCode` (out of scope).
+- Do NOT model `object.Equals` deeply (it adds complexity without insight).
+- DO model the `==` and `!=` operators as wrappers over `Equals`.