Repository navigation
Conversation
The reviewed formal guides predate the Python port. Every statement about which ports replay the corpus, carry a replay mechanism or must be exercised now names TypeScript, Go, Rust and Python, checked against the validation targets, the conformance inventory and the hosted workflow. Native mutant mappings, generated-cohort fault detection and the causal publication monitor stay scoped to the ports that have them. Refresh the source-audit guide pins and the go-parity source-audit hash.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #226 +/- ##
==========================================
- Coverage 93.73% 93.73% -0.01%
==========================================
Files 78 78
Lines 11357 11357
Branches 656 656
==========================================
- Hits 10646 10645 -1
- Misses 641 642 +1
Partials 70 70
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
lan17
added a commit
that referenced
this pull request
Oct 24, 2026
## Problem DialCache is built by one maintainer and many coding agents that open pull requests from his account. The rules those agents followed were spread across `AGENTS.md` convention bullets, `AUTHORING.md`, `VALIDATION.md`, `docs/authoring.md` and `docs/maintainers.md`, and the reasons behind designs lived in rewritten issue bodies, a folder on one laptop and Claude memory. The history shows the cost: - #190, #197, #198 and #213 merged without a full formal run on their head. #198 left the exploration lane red on `main` for three weekly runs. - #219 exported `CacheUseCaseOptions` against #218's design, and #218's decision checklist was never ticked. - #132 reversed #60 without linking it. #117's body was rewritten six times, so its rejected design survives only in GitHub's edit history. - An agent merged four PRs in one session, and agent reviews posted from the maintainer's account read like approvals. - The one validation tier, a 2.5-hour full run, was either skipped or re-run on intermediate pushes: 115 runs in a month, 63 of them green on commits later superseded. This began as an evaluation of OpenSpec. Its `specs/` tree would restate behavior that Quint and `CONTRACTS.md` already define, with no IDs and a hardcoded grammar, so only its change-record idea was adopted, as a plain convention with no CLI. ## Change Type: Docs plus Tooling (the formal workflow and the docs link checker). No design record: this PR defines the convention. ### The process in one line Classify the change; stop where only the maintainer decides; follow the steps for the type; validate at the tier the change needs; open a draft PR; leave draft when the finish list holds; the maintainer merges. ### 1. Classify the change `AGENTS.md` opens with a table of nine change types. The type fixes three things: whether a design record is needed, which path of steps applies, and which validation tier the PR needs before it leaves draft. | Type | Record | Tier | | --- | --- | --- | | Portable behavior: a `CONTRACTS.md` obligation added, changed or removed; a new conformance profile | Required | Full | | Bug fix | No, unless it reverses a recorded decision | Replay; Mutations if the mutant rule fires; Full if a Quint transition, invariant or challenge changes | | Public API | When every port must mirror it, or it reshapes how callers construct or call the cache | Replay; Mutations if the mutant rule fires | | Docs | No | PR CI | | Refactor or move | No | PR CI; Replay if port source, a `.qnt` file or a replay driver changes; Full with exploration for a move | | Formal infrastructure | When it changes how conformance is established | Full | | Tooling | No | PR CI; Full if a Quint or language toolchain pin changes | | New port | Required | Full | | Release | No | Maintainer only | A change spanning types follows every matching path and the strictest tier. Any change that reverses a decision made in an earlier record, issue or pull request needs a record. The mutant rule fires when a change edits a file that an entry in `mutations.json` or `rust-mutations.json` names, or edits those catalogs. ### 2. Write a design record before the code A record is one Markdown file under `design/`, written from `design/TEMPLATE.md`: context, proposal, out of scope, contract and model changes, decisions, impact, plan and deviations. - Each decision starts `Open`. Only the maintainer confirms one, and the record links or quotes the approval. A comment or review an agent wrote is not an approval, whichever account posted it. - Implementation starts when every decision is confirmed and the record is `Accepted`. - A changed decision keeps its earlier choice under Rejected, with the reason, so the history stays readable. The record returns to `Proposed` and the PR to draft until the new choice is confirmed. - Any departure of the built behavior or API from the record goes under Deviations in the same PR. - Records explain decisions; they never define behavior. Quint, `CONTRACTS.md`, `SPEC.md`, `PROTOCOL.md` and `docs/` do, and documentation never cites a record as the source of a guarantee. Before changing a feature, an agent searches `design/`, issues and pull requests for the contract IDs and API names, and runs `node formal/tools/where.mjs <ID>` for each contract involved. ### 3. Stop at the gates A gate is a decision only the maintainer makes. An agent that reaches one asks in the session; when he is away it pushes a draft PR with the open questions in the description and ends its turn. The gates: 1. a design decision; 2. a change to a confirmed decision; 3. unsettled scope, including a request the repository contradicts; 4. a required validation lane that could not run, timed out or was cancelled; 5. anything irreversible: merging, enabling auto-merge, pushing to `main`, dispatching `Release`, deleting a branch or tag, changing repository settings. Approval is the maintainer's own words, typed in a session or written by him on GitHub. Every issue, comment or review an agent posts begins with `Agent:`, and an agent never submits an approving review, because GitHub would count an approval from his account. ### 4. Validate at the tier the change needs `formal-full.yaml` now takes a `mode` input. Each mode adds to the one before it. | Tier | What runs | Time | When | | --- | --- | --- | --- | | PR CI | native tests, Redis/Valkey/Cluster integrations, smoke histories, ledger audit, docs build; differential shards when a Quint input changes | about 6 min | every push | | Replay (`mode=replay`) | generate the corpus, or restore it from the cache, then replay it in all four ports, plus the symbolic lane | about 8 min cached, 17 on a miss | port, replay-driver and regression-only changes | | Mutations (`mode=mutations`) | Replay plus the TypeScript, Go and Rust mutation campaigns | about 50 min | a file a catalogued mutant rewrites, or a mutant catalog, is edited | | Full (`mode=full`, the default) | Mutations plus the Quint model checks and the model-fault campaign | about 2.5 h | Quint transitions, invariants or challenges, the kernel library, the Quint toolchain; weekly on `main`, with exploration | Why the split is safe: 136 of the full run's minutes are the model-fault campaign, which reads only the Quint models, the challenge catalog and the Quint toolchain, so a port change cannot alter its result. Lanes a mode does not select are skipped, and the aggregate requires them to report *skipped*, so a run cannot pass as a stronger mode than it ran. The run name carries the mode, and the concurrency group is keyed by ref and mode, so a replay never queues behind a full run. The corpus is cached under an exact hash of every generation input: the models, `formal/replay/`, `formal/tools/`, `formal/generated/`, the catalogs other than the three review ledgers and the style allowlist, the committed witness fixtures, the Quint pin, the `Makefile` and the package manifests, with Markdown excluded. Generation is deterministic in content, so a hit equals a fresh corpus, and only an exact key may restore. A branch that adds Quint regressions misses the cache and regenerates, so its histories enter the corpus every port must pass. The weekly run regenerates even on a hit. Committing the corpus was rejected: it is 35 MiB and changes on every model edit, and the 17 smoke histories already are the committed subset. The tier runs once, on the final candidate, after review comments are addressed and PR CI is green. A green run on an earlier commit covers the head when PR CI is green there and the difference is only Markdown or ledger pins; anything else, a rebase included, needs a new run. ### 5. Open the PR and finish PRs open as drafts from `.github/pull_request_template.md` (Problem, Change, Open questions, Ports, Validation, Follow-ups). A PR leaves draft only when every step of its path is done, its record is `Accepted` or `Implemented`, its tier is green on the head, no open questions remain, and the description reads true as the squash commit body. Commits and descriptions carry no Co-Authored-By trailer, generated-by footer or agent signature. ### What changed, file by file - **`AGENTS.md`**: rewritten around "Make a change": classify, gates, one path per type, ledgers, validate, open, finish. Critical behavior and the conventions stay; the directory tree goes, and the stale claims it carried are corrected. Main's rule about the course under `formal/guides/course/` is merged in. - **`CLAUDE.md`**: `@AGENTS.md`, for Claude Code builds that read only `CLAUDE.md`. - **`DEVELOPMENT_PROCESS.md`**: the same process for human readers, with Mermaid diagrams: how behavior is defined, the life of a change, the record lifecycle, and a portable feature end to end. `AGENTS.md` requires a change to its process section to update this guide in the same PR. - **`design/README.md`, `design/TEMPLATE.md`**: when a change needs a record, how to find earlier decisions, the record lifecycle, the template. - **`.github/pull_request_template.md`**: the description shape agents fill with `--body-file`. - **`.github/workflows/formal-full.yaml`**: the `mode` input, lane conditions, per-mode gate, run name with the mode, concurrency group per ref and mode, corpus cache restore and save, weekly regenerate on a hit. - **`typescript/test/formal-validation.test.ts`**: pins the mode options and default, the lane conditions, the exact cache key and restore step id, the step order, and the gate line for line. Flipping one gate expectation fails it. - **`formal/guides/VALIDATION.md`, `AUTHORING.md`, `docs/maintainers.md`, `formal/README.md`, `GLOSSARY.md`, course lessons 14 and 17**: the tiers replace "full validation before merge"; the reviewed-guide pins are re-keyed with `check-source-audit.mjs --refresh`. - **`formal/catalogs/README.md`**: "Refresh after an edit", the ordered recipe over #228's `--refresh` and `--refresh-inputs` commands. - **`scripts/check-docs.mjs`**: `AGENTS.md`, `DEVELOPMENT_PROCESS.md` and `design/README.md` join the relative-link check, with a test. ### Decisions the maintainer confirmed in session (2026-10-24) - Implementation waits until a design record is `Accepted`. - Every issue, comment or review an agent posts begins with `Agent:`. - Pull requests opened before records existed, such as #219, need no backfilled record; their review checks the decisions in their issue. - `AGENTS.md` stays one file (321 lines, 21.7 KB). - No agent signatures in commits or PR descriptions. ### Left out on purpose - OpenSpec's `specs/` tree and CLI. - Committing the generated corpus; the cache gives the same skip with no history cost. - Mechanical tier selection. The agent picks the mode from the table, and the weekly `full` run on `main` is the backstop. - Backfilled records for #218/#219 and the PR template as a GitHub-applied template: GitHub never applies one to `gh pr create --body`, so `AGENTS.md` carries the rule. ## Ports | Port | Status | | --- | --- | | TypeScript | N/A: no port code changed; only the workflow-shape test under `typescript/test/` | | Go | N/A | | Rust | N/A | | Python | N/A | ## Validation Head: `dd7b2fd`. The last commit changed only `design/README.md`, so the runs on `8d5cec1` cover it under the carry-over rule once PR CI is green there. - PR CI at `dd7b2fd`: every check green, `test`, `quint`, `differential (1)` to `(4)`, `Build documentation` and `Validate PR title` included. - Formal replay 40118275863 (`replay`) at `8d5cec1`: green. Cache miss, because this commit changed the key; generate 10 min 45 s; the parity lanes then waited about nine minutes for runners behind the concurrent mutations run; 29 min wall. - Formal mutations 40118278589 (`mutations`) at `8d5cec1`: green in 46 min 28 s. All 19 mutation shards and their three merges passed, `check-models` was skipped as the mode requires, and the aggregate accepted that combination, so the `mutations` gate arm and the `inputs.mode != 'replay'` lane conditions have run once before merge. - Earlier replay runs on this branch, all green: 38612947384 at `296eede` (miss, 17 min 14 s), 38613028985 at `296eede` (hit, 8 min 16 s), 38617177083 at `6490055` (hit, 6 min 11 s), 38651601005 at `8667553`, 38702974816 at `788142a` and 40116954099 at `95e00c3` (misses after merges of `main`, 15 to 19 min). - Local at `8d5cec1`: `make audit`, including the ledger checks, the course citations and the Quint style caps; 86 tests across `formal-validation`, `formal-course`, `formal-style`, `formal-source-audit` and `formal-go-parity`; the `scripts/check-docs` tests and link check over 53 pages; every anchor into the rewritten `formal/README.md` resolves. - Reviews, simulation only: three competing `AGENTS.md` shapes judged against a rule inventory and a study of agent failures in #176 to #225; six simulated agents walked the result through real tasks; a fact-checker verified every claim against the repo and the ruleset; four reviewers checked the mode and cache change; a three-lane review of the merged branch against current `main`. Their fixes are in this head. Not run: `full` mode on this branch. The PR changes no model, challenge or Quint input, so `replay` is its tier; the `full` arm's only changes are the per-mode concurrency group and the schedule condition, exercised by the replay runs through the same file. ## Follow-ups - #226 edits the same guides; whichever of #225 and #226 merges second re-keys three ledger lines. - The model-fault campaign runs 145 of its 150-minute budget (#219 hit it). Sharding it, or persisting its per-closure cache across runs, would let a regression-only change re-measure one profile's cells in minutes. - Cheap PR checks that would have caught past breakage: compile every catalogued mutant (#190), reject tracked symlinks (#198), run the 36-second Apalache check in PR CI. - Dropping Mutations as a pre-merge tier, with weekly measurement plus the compile check in its place, is a candidate simplification; the mode stays available either way. - `BEHAVIOR.md`, `GO-PARITY.md`, `SEMANTIC-COVERAGE.md`, `PORTING.md`, `WALKTHROUGH.md`, `go/README.md` and `docs/authoring.md` still say behavior changes need full validation. That is stricter than the new policy, so it is harmless until their next ledger refresh.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
The reviewed formal guides predate the Python port (#200).
formal/catalogs/profiles.jsondeclares all 17 profiles fortypescript,go,rustandpython,make formalrunsformal-python, and the full formalworkflow gates on a
python-paritylane. The guides still described two or threeports. Step 4 of AUTHORING.md's "Codifying the next behavior", the workflow
agents follow for new behavior, said to replay "in TypeScript, Go and Rust".
What
Every statement about which ports replay the corpus, carry a replay mechanism or
must be exercised now names TypeScript, Go, Rust and Python. Each was checked
against
formal/tools/validation.mjs,formal/tools/conformance.mjs,formal/tools/explore.mjs,.github/workflows/formal-full.yamlandpython/tests/before it changed.walkthrough pointer; Python 3.11+ and
python/.venvsetup in theprerequisites;
make formal-pythonin the lane list; seven parallel hostedlanes (four parity, three mutation) instead of six.
summary and step 4. The fault-detection paragraph now says Python has no
native mutation campaign.
command that replays the example history.
JSON-lines coordinator transport; each port's no-settle control (Rust and
Python already have one); the Python
prepare, adapter andcheckcommands,default source inventory and witness-evidence inputs.
formal-summaryartifact and exploration ordering.make mutationscoversTypeScript, Go and Rust only.
TEST-AUDIT, TEST-MAP: replay statements that said "both ports" or
"TypeScript and Go" now say every port or list all four.
go-parity.json
sourceAuditSha256. Only hashes and line numbers changed.This PR changes no Quint models, profiles, replay code or behavior.
Left scoped to fewer ports on purpose
nativeMutants, themutations.jsonsections),generated-cohort fault detection and the mutation boundary gate cover
TypeScript and Go only. Rust keeps its note about its separate catalog.
feature-coverage.jsonname only TypeScript and Go tests.drivers. SPEC.md and SEMANTIC-COVERAGE.md now name those three instead of
"both drivers".
two-port runs and stay as history.
Design-record pointers skipped
#225 adds
design/README.mdbut has not merged;design/README.mdis not onorigin/main. This PR therefore leaves out the design-record row informal/README.md's task table and the opening sentence in AUTHORING.md's
"Codifying the next behavior". Both can follow once #225 lands.
Gaps noticed, not changed
PORTING.md's "New-port acceptance" asks for representative semantic mutations.
formal/tools/explore.mjsstill logs "both native witness leaves record theshortfall" when the tolerated witness step fails.
Verified
make auditandnode scripts/check-docs.mjspass on Node 24.20.0, as doestypescript/test/formal-source-audit.test.ts.heldPolicyDoesNotSpendSourceBudgetTestwith Quint 0.32.0, thennode formal/tools/run-python-replay.mjs --profile=source-budgets --trace=…passed (1 case, 8 steps).