From 1e33b43c25170536b40d4322c6232e3fb4029c8b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 27 Dec 2025 02:47:59 +0000
Subject: [PATCH] Add documentation for TLA+ CI verification

Co-authored-by: johndoe6345789 <224850594+johndoe6345789@users.noreply.github.com>
---
 README.md         | 14 ++++++++++++++
 scripts/README.md | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 scripts/README.md

diff --git a/README.md b/README.md
index 9f9c251..a50bba8 100644
--- a/README.md
+++ b/README.md
@@ -163,6 +163,20 @@ The API will:
 - **GitLab**: Use personal access tokens with `read_api` and `read_repository` scopes
 - Tokens can be passed via `--token` flag or environment variables (`GITHUB_TOKEN`, `GITLAB_TOKEN`)
 
+## Formal Verification
+
+WizardMerge includes a formal TLA+ specification that is verified in CI:
+- **Specification**: [spec/WizardMergeSpec.tla](spec/WizardMergeSpec.tla)
+- **CI Workflow**: `.github/workflows/tlc.yml`
+- **Verification Script**: `scripts/tlaplus.py`
+
+The specification is automatically checked on every push to ensure:
+- Syntax correctness
+- Module structure validity  
+- Type checking of invariants and temporal properties
+
+See [scripts/README.md](scripts/README.md) for details on running the verification locally.
+
 ## Research Foundation
 
 WizardMerge is based on research from The University of Hong Kong achieving:
diff --git a/scripts/README.md b/scripts/README.md
new file mode 100644
index 0000000..192f0fb
--- /dev/null
+++ b/scripts/README.md
@@ -0,0 +1,41 @@
+# Scripts
+
+This directory contains utility scripts for the WizardMerge project.
+
+## tlaplus.py
+
+TLA+ Model Checker runner for continuous integration.
+
+### Usage
+
+```bash
+python3 scripts/tlaplus.py run
+```
+
+### What it does
+
+1. **Downloads TLA+ Tools**: Automatically downloads the TLA+ tools JAR file (containing TLC model checker and SANY parser) to `.tlaplus/` directory if not already present.
+
+2. **Parses Specification**: Runs the SANY parser on `spec/WizardMergeSpec.tla` to verify:
+   - Syntax correctness
+   - Module structure validity
+   - Type checking
+
+3. **Generates Output**: Saves parsing results to `ci-results/WizardMergeSpec_parse.log`
+
+### CI Integration
+
+This script is used in the `.github/workflows/tlc.yml` GitHub Actions workflow to:
+- Verify the TLA+ specification on every push and pull request
+- Catch syntax errors and structural issues early
+- Provide formal verification that the merge algorithm specification is well-formed
+
+### Note on Model Checking
+
+The WizardMergeSpec is a parametric formal specification that defines constants requiring concrete values for full model checking. This script performs syntax validation and type checking, which is appropriate for CI purposes. Full TLC model checking would require creating test harness modules with specific constant instantiations.
+
+### Requirements
+
+- Python 3.6+
+- Java 11+ (for running TLA+ tools)
+- Internet connection (for initial download of TLA+ tools)