Skip to content

docs(formal): align current pickup routing after #393 #400

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
d6g8k5htny-coder merged 1 commit into from
Oct 14, 2026
Merged

docs(formal): align current pickup routing after #393 #400

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 9 additions & 6 deletions formal/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
8 changes: 5 additions & 3 deletions formal/REVIEW_LANE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
4 changes: 2 additions & 2 deletions formal/manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down