refactor(verification): complete formal verifier retirement

CONTRIBUTING.md

@@ -30,7 +30,7 @@ safe-docx/
 ├── skills/                Agent instructions for document editing
 ├── docs/                  User and maintainer guides
 ├── spec-compliance/       ECMA-376 registry, schemas, and reports
-├── verification/          Invariants and optional formal verification
+├── verification/          Runtime and release-verification evidence
 ├── openspec/              Requirements and change proposals
 ├── tests/                 Cross-package fixtures and integration tests
 └── site/                  Public documentation site
@@ -190,7 +190,7 @@ npm run check:conformance-citations && \
 npm run check:conformance-doc
 ```
 
-Also run checks specific to the changed surface, including generated tool docs, site links, package manifests, or formal verification where applicable.
+Also run checks specific to the changed surface, including generated tool docs, site links, package manifests, or release-verification evidence where applicable.
 
 ## Pull Requests
 

openspec/changes/remove-lean-verification-subsystem/design.md

@@ -0,0 +1,31 @@
+# Design: Complete Lean subsystem retirement
+
+## Principle
+
+Retirement is atomic at the architectural boundary: no Lean executable,
+supervisor, option, certificate field, workflow, or normative requirement may
+remain. Historical archived proposals may retain their record, but current
+specification and live guidance must describe the post-retirement system.
+
+## Coverage migration
+
+Before deletion, inventory every non-duplicated behavioral invariant exercised
+only through Lean. Re-express user-visible invariants—package admission limits,
+relationship safety, move/comment/note topology, accept/reject behavior, and
+fail-closed parsing—as TypeScript unit, property, or corpus regression tests.
+Proof-internal claims with no runtime behavioral counterpart are retired rather
+than translated into pretend proofs.
+
+## API transition
+
+Remove `leanXmlVerifier` configuration, `LeanXmlVerifierOptions`,
+`runLeanXmlTripleVerifier`, and Lean certificate output. Because these are
+exported surfaces, release notes must call out the breaking removal. No inert
+compatibility flag remains.
+
+## OpenSpec transition
+
+Canonical Lean requirements are removed from `docx-comparison`; behavioral
+requirements that remain product requirements are rewritten without naming an
+implementation language or proof system. Active Lean proposals are marked as
+superseded by this change before archival.

openspec/changes/remove-lean-verification-subsystem/inventory.md

@@ -0,0 +1,41 @@
+# Retirement inventory and coverage map
+
+The complete implementation was already present on `main` in commit `55df2b94`
+(`refactor: replace Lean verification with artifact checks`). This audit records
+the resulting state and the maintained TypeScript evidence that replaced the
+removed subsystem.
+
+## Removed surfaces
+
+| Surface | Post-retirement state |
+| --- | --- |
+| Source and build | `verification/lean`, its toolchain files, build artifacts, and audit scripts are absent. |
+| CI | `.github/workflows/lean-build.yml` is absent. |
+| Runtime | The comparison pipeline has no checker subprocess branch or executable discovery. |
+| Public API | `leanXmlVerifier`, `LeanXmlVerifierOptions`, `runLeanXmlTripleVerifier`, and certificate fields are absent. |
+| Integration tests | Differential, specification-bridge, and checker-supervisor suites are absent. |
+| Current specification | Canonical comparison and conformance specifications contain no formal-verifier requirement. |
+| Current claims | Generated capability and conformance surfaces contain no formal-assurance claim. |
+
+## Preserved user-visible invariants
+
+| Invariant | Maintained TypeScript evidence |
+| --- | --- |
+| Emitted-redline LCS minimality | `packages/docx-release-verifier/src/minimality.ts` and `minimality.test.ts` |
+| Accept/reject text projection | `packages/docx-release-verifier/src/verifier.ts` and `verifier.test.ts`; `packages/docx-core/src/integration/accept_reject_invariant_corpus.test.ts` |
+| Field structure under comparison and resolution | `packages/docx-compare/src/baselines/atomizer/pipeline.field-validation.test.ts`; complex-field reconstruction tests; docx-core field regressions |
+| Package and relationship integrity | release-verifier package gates; docx-compare relationship collision and ancillary-story tests |
+| Comment and note topology | docx-compare comment/ancillary-note tests and docx-core acceptance/rejection integration tests |
+| Move-range pairing and paragraph-mark resolution | docx-compare move-range and in-place modifier regressions |
+| Real implementation cross-check | `packages/docx-core/src/integration/libreoffice-oracle-trust-boundary.test.ts` when LibreOffice is available |
+
+Proof-internal propositions with no observable product behavior were retired;
+they were not relabeled as runtime guarantees.
+
+## Residual-reference classification
+
+Current product code, public APIs, workflows, canonical specs, and generated
+claims contain no retired-subsystem references. Historical OpenSpec material is
+retained only as change history. The retirement proposal itself necessarily
+names the removed surface, and negative claim tests continue to reject generic
+formal-assurance language.

openspec/changes/remove-lean-verification-subsystem/proposal.md

@@ -0,0 +1,34 @@
+# Change: Retire the Lean verification subsystem
+
+## Why
+
+Lean verification was expected to have been removed, but the repository still
+contains an active CI workflow, a compiled checker and proof tree, public
+TypeScript options, production pipeline integration, differential/bridge tests,
+quality-gate rules, and normative OpenSpec requirements. The remaining verifier
+also currently fails the ordinary paragraph-mark insertion case, blocking the
+otherwise unrelated pre-submit suite. Removing only that test would conceal the
+larger architectural inconsistency.
+
+## What Changes
+
+- Remove the `verification/lean` project and Lean-specific CI workflow.
+- Remove the TypeScript Lean checker supervisor, public configuration/options,
+  exports, certificates, and atomizer pipeline branch.
+- Remove Lean-only bridge, differential, and integration tests and scripts.
+- Remove or rewrite quality-gate, traceability, and documentation references.
+- Retire active Lean-specific OpenSpec changes and remove Lean-specific
+  normative requirements from the canonical comparison specification.
+- Preserve behaviorally important OOXML invariants as ordinary TypeScript
+  regression/property tests before deleting any Lean-only coverage.
+
+## Impact
+
+- **BREAKING** for callers using `leanXmlVerifier` options or
+  `runLeanXmlTripleVerifier` directly
+- Affected specs: `docx-comparison`
+- Affected code: `verification/lean`, `.github/workflows/lean-build.yml`,
+  `packages/docx-compare`, Lean bridge/differential tests in `docx-core`, and
+  Lean-specific repository documentation and scripts
+- OpenSpec cleanup: active `verify-lean-*` changes must be superseded or closed
+  explicitly rather than left as impossible work

openspec/changes/remove-lean-verification-subsystem/specs/docx-comparison/spec.md

@@ -0,0 +1,27 @@
+## ADDED Requirements
+
+### Requirement: Comparison integrity is enforced without an external Lean verifier
+
+The comparison pipeline SHALL enforce its supported package, relationship,
+story-topology, and accept/reject integrity requirements through maintained
+runtime validation and TypeScript regression or property tests, without a Lean
+executable or Lean-specific public API.
+
+#### Scenario: Comparison runs without a Lean toolchain
+
+- **GIVEN** a supported comparison input on a machine with no Lean installation or compiled checker
+- **WHEN** comparison runs
+- **THEN** all required runtime integrity checks SHALL execute without invoking Lean
+- **AND** the result SHALL contain no Lean-specific certificate or not-run state
+
+#### Scenario: Former verifier option is absent
+
+- **GIVEN** the post-retirement public comparison API
+- **WHEN** a caller inspects its options and exports
+- **THEN** `leanXmlVerifier`, `LeanXmlVerifierOptions`, and `runLeanXmlTripleVerifier` SHALL not be present
+
+#### Scenario: Behavioral coverage survives retirement
+
+- **GIVEN** an OOXML case whose user-visible invariant was previously checked only by Lean integration
+- **WHEN** the Lean subsystem is removed
+- **THEN** an equivalent TypeScript regression, property, or corpus test SHALL protect that invariant before deletion

openspec/changes/remove-lean-verification-subsystem/tasks.md

@@ -0,0 +1,28 @@
+## 1. Inventory and coverage preservation
+
+- [x] 1.1 Inventory Lean-only runtime, CI, API, documentation, and spec surface
+- [x] 1.2 Map each user-visible Lean-checked invariant to existing TypeScript coverage
+- [x] 1.3 Add missing TypeScript regression/property coverage before removal
+
+## 2. Runtime and API removal
+
+- [x] 2.1 Remove the Lean verifier supervisor and tests
+- [x] 2.2 Remove atomizer pipeline integration, options, exports, and certificate fields
+- [x] 2.3 Remove Lean-dependent integration and differential tests
+
+## 3. Build and repository removal
+
+- [x] 3.1 Remove `verification/lean` and `.github/workflows/lean-build.yml`
+- [x] 3.2 Remove Lean-only scripts, caches, quality-gate rules, and traceability entries
+- [x] 3.3 Update contributor and release documentation
+
+## 4. Specification cleanup
+
+- [x] 4.1 Remove Lean-specific canonical `docx-comparison` requirements
+- [x] 4.2 Rewrite retained behavioral requirements without Lean coupling
+- [x] 4.3 Supersede and archive active `verify-lean-*` changes
+
+## 5. Verification
+
+- [x] 5.1 Confirm no live Lean references remain outside archived history
+- [x] 5.2 Run the full repository pre-submit suite

scripts/check_advanced_revision_classification.mjs

@@ -153,7 +153,7 @@ async function validateEvidence(record, operationStatuses, executedClaimsByEvide
 
   for (const [operation, status] of operationStatuses) {
     if (!ALLOWED_STATUSES.has(status)) throw new Error(`${record.id}: invalid ${operation} status ${status}`);
-    if (status === 'non-goal' || operation.startsWith('lean.')) continue;
+    if (status === 'non-goal') continue;
     const covered = evidenceByOperation.get(operation) ?? new Set();
     const missing = record.elements.filter((element) => !covered.has(element));
     if (missing.length > 0) throw new Error(`${record.id}: ${operation} lacks element-specific evidence for ${missing.join(', ')}`);

scripts/generate_capability_projection.test.mjs

@@ -314,5 +314,5 @@ test('the human report retains the neutral evidence limitations', async () => {
   const report = await readFile(path.join(root, 'spec-compliance/generated/safe-docx-capability-projection.md'), 'utf8');
   assert.match(report, /a positive row applies only to the listed evidence and scope/);
   assert.match(report, /explicit untested and gap rows/);
-  assert.doesNotMatch(report, /formal assurance|theorem prover|Lean/i);
+  assert.doesNotMatch(report, /formal assurance|theorem prover/i);
 });

verification/ROADMAP.md

@@ -1,14 +1,9 @@
 # Verification roadmap
 
-## Lean retirement (2026-08-13)
+## Release verification model
 
-Safe DOCX previously maintained a Lean verification program in this location.
-That program was removed because its local toolchain and multi-minute build made
-the release certificate non-portable and routinely `not_run` in the environment
-where documents are actually reviewed.
-
-This changes the mechanism, not the release standard. The independent
-TypeScript release verifier operates on the finished DOCX artifact and requires:
+The independent TypeScript release verifier operates on the finished DOCX
+artifact and requires:
 
 - exact accept-all and reject-all text projections;
 - emitted-redline LCS minimality;
@@ -18,5 +13,3 @@ TypeScript release verifier operates on the finished DOCX artifact and requires:
 
 The release verifier remains separate from the redline generator so the
 implementation producing a document does not certify its own in-memory model.
-Historical Lean design work remains available in Git history; it is not a
-current product claim, runtime dependency, or release gate.