[docs] Update glossary - daily scan

[Evangelink]

Glossary Updates

Scan Type: Incremental (daily) — Thursday 2026-04-30

Terms Added:

• Informal Spec (FV): Defines the Phase 2 formal-verification artifact (natural-language property list) that bridges research and Lean 4 proof-writing. Introduced by formal-verification/REPORT.md in commit 485bb51 but was missing from the glossary, leaving the FV target lifecycle unexplained at that step.

Changes Analyzed:

• Reviewed 1 commit from the last 24 hours
• Commit 485bb51: [Lean Squad] feat(ci): Task 9 — FV docs validation workflow + updated REPORT.md

Related Changes:

• Commit 485bb51a: Added fv-docs-validation.yml CI workflow and created formal-verification/REPORT.md introducing the "Informal Spec" concept across multiple references.

Generated by Glossary Maintainer · ● 394.1K · ◷

• expires on May 2, 2026, 12:54 PM UTC

---

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

# Create a new branch
git checkout -b docs/glossary-daily-2026-04-30-fedeaa4042f4dcf5

# Apply the patch (--3way handles cross-repo patches where files may already exist)
git am --3way /tmp/agent-25166259903/aw-docs-glossary-daily-2026-04-30.patch

# Push the branch to origin
git push origin docs/glossary-daily-2026-04-30-fedeaa4042f4dcf5

# Create the pull request
gh pr create --title '[docs] Update glossary - daily scan' --base main --head docs/glossary-daily-2026-04-30-fedeaa4042f4dcf5 --repo microsoft/testfx

Show patch (34 lines)

From a002a280c396fb660078fc4be49faef56dd8e73b Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Thu, 30 Apr 2026 12:52:08 +0000
Subject: [PATCH] docs: add Informal Spec (FV) to glossary

Add definition for the 'Informal Spec' FV concept introduced by recent
formal-verification work (commit 485bb51). The term recurs in
formal-verification/REPORT.md and specs/ but was not yet defined in the
glossary, leaving Phase 2 of the FV target lifecycle unexplained.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 docs/glossary.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/docs/glossary.md b/docs/glossary.md
index 34725a7..fde40d0 100644
--- a/docs/glossary.md
+++ b/docs/glossary.md
@@ -46,6 +46,10 @@ An MTP extension (`Microsoft.Testing.Extensions.HangDump`) that captures a proce
 
 ## I
 
+### Informal Spec (FV)
+
+An intermediate artifact in the [Formal Verification (FV)](#formal-verification-fv) workflow that documents the behavioural properties of an [FV Target](#fv-target) in plain English (or structured natural language), before writing formal [Lean 4](#lean-4) proofs. An informal spec lists preconditions, postconditions, edge-case expectations, and any confirmed bugs discovered during analysis. It corresponds to Phase 2 of the FV target lifecycle and lives in the `formal-verification/specs/` directory.
+
 ### IsTestingPlatformApplication
 
 An MSBuild property (`<IsTestingPlatformApplication>true</IsTestingPlatformApplication>`) that marks a project as an MTP test application. When set, the project builds into a self-contained test runner executable rather than a class library consumed by a separate test host.
-- 
2.53.0