diff --git a/formal/README.md b/formal/README.md
index f4dfa173f..f762662e0 100644
--- a/formal/README.md
+++ b/formal/README.md
@@ -2,9 +2,11 @@
 
 Scientific effect: **NONE**. This directory is the second package in the
 repository's formal-verification lane. The lane's contract is the
-[formal-verification guide](../docs/FORMAL_VERIFICATION.md); the lane is
-coordinated in [work item #95](https://github.com/d6g8k5htny-coder/main/issues/95);
-the first package is the
+[formal-verification guide](../docs/FORMAL_VERIFICATION.md); new work is claimed in
+the relevant current pull request or work discussion under the
+[current workflow](../governance/OP-WORKFLOW-20260930.md).
+Closed [work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) is the
+historical rollout record; the first package is the
 [Math- pilot](https://github.com/d6g8k5htny-coder/Math-/tree/cc2989c1280f4f227d0c6aa30c8841d6ba01e46e/formal)
 (13 GP-FOR-192 scalar companions, Lean 4 + Mathlib). This package follows the same
 manifest, status, gate and alignment contract and adds nothing to the
@@ -120,9 +122,10 @@ tree. See the rollout record for the coordination items.
 - [docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md](../docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md)
   — what this package adds, how it converged onto the Math- contract, what is
   asked of other repositories and agents, and this session's capability limits.
-- [Work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) — record
-  actual pickup of alignment review or of the remaining "Numerical formalizer"
-  steps there.
+- [Work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) — historical
+  rollout record. Record actual pickup of alignment review or of the remaining
+  "Numerical formalizer" steps in the relevant current pull request or work
+  discussion under the [current workflow](../governance/OP-WORKFLOW-20260930.md).
 
 ## What this package does not do
 
diff --git a/formal/REVIEW_LANE.md b/formal/REVIEW_LANE.md
index 16eeb6d91..ff64b1c4b 100644
--- a/formal/REVIEW_LANE.md
+++ b/formal/REVIEW_LANE.md
@@ -84,6 +84,8 @@ hash, new `--run-lean` receipt) or fix the anchor, then re-review.
 All 31 targets: authored by Anthropic / Claude via a Cursor cloud agent on
 2026-09-27; `proved` at source; `kernel-checked` only in the receipt of a
 trusted run; alignment `PENDING_INDEPENDENT_REVIEW`. No record other than the
-template exists. Record actual pickup in
-[work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) so two
-reviewers do not duplicate the work.
+template exists. Record actual pickup in the relevant current pull request or work
+discussion under the [current workflow](../governance/OP-WORKFLOW-20260930.md) so two
+reviewers do not duplicate the work. Closed
+[work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) remains the
+historical rollout record.
diff --git a/formal/manifest.json b/formal/manifest.json
index 8d4318869..72b2644b3 100644
--- a/formal/manifest.json
+++ b/formal/manifest.json
@@ -39,8 +39,8 @@
     "formal/sources/side24_v1/ENCLOSURE.json": "72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811",
     "formal/SCOPE.md": "fd06700628b1fbc81c5cfe3786aaa455032375bcb879914f068a66b726802a17",
     "formal/GLOSSARY.md": "342d4efb374fea31c39e51f8f6bcdbc50d7fb5fea1fd393eda21afff92c62fb8",
-    "formal/README.md": "1398c3c6d15476afe9d4ef01fc98fb199976907123b438ae1743f4e87e31e007",
-    "formal/REVIEW_LANE.md": "6a0dcdd93f1aec16ede829820b913116a5c60c2bbbd78630690599dbc5d8be41",
+    "formal/README.md": "4e6302e9174b7b6b601238674c7eab8934ccb2240e2fc99cd3936d486d81b71a",
+    "formal/REVIEW_LANE.md": "84aba7776af4beff706a26ec67abef86c24641966b84aba67498983346f1d75a",
     "formal/reviews/TEMPLATE_alignment_review.json": "e722e928ca43c16981e063d8eb1c91e9bf8c683241d9dcf156400a419e72feb3",
     "formal/reviews/README.md": "333ca71e7c676cee89e5d01cd61999c21bb0584e41d6bdacb18afa410109f95d",
     "tools/formal_gate_check.py": "21c355e02ac6e01337d10465a3105b34b93f832586ee60aa2430f662a90cd8b7",