[lan17]

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:

• feat(go): reshape the public API for Go idioms and tag the module with each release #190, refactor: move TypeScript package under typescript/ #197, ci: publish Rust with the shared release version #198 and refactor(go): extract private helpers and move standalone tests #213 merged without a full formal run on their head. ci: publish Rust with the shared release version #198 left the exploration lane red on main for three weekly runs.
• feat: add exact-key deletion across all ports #219 exported CacheUseCaseOptions against Add exact-key delete for one cached result (child of #217) #218's design, and Add exact-key delete for one cached result (child of #217) #218's decision checklist was never ticked.
• feat(redis): transparent zstd compression for large cache values #132 reversed Add thresholded client-side compression for Redis payloads #60 without linking it. Add opt-in stale-on-error recovery from retained Redis values #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 feat(formal): add in-repo ledger refresh commands #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 feat: add exact-key deletion across all ports #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 Add exact-key delete for one cached result (child of #217) #218/feat: add exact-key deletion across all ports #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 test(formal): parse the witness corpus once in the completion gates #176 to docs: define the agent change process and in-repo design records #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

• docs(formal): describe all four ports in the formal guides #226 edits the same guides; whichever of docs: define the agent change process and in-repo design records #225 and docs(formal): describe all four ports in the formal guides #226 merges second re-keys three ledger lines.
• The model-fault campaign runs 145 of its 150-minute budget (feat: add exact-key deletion across all ports #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 (feat(go): reshape the public API for Go idioms and tag the module with each release #190), reject tracked symlinks (ci: publish Rust with the shared release version #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.

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 93.73%. Comparing base (6b8452f) to head (dd7b2fd).

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #225   +/-   ##
=======================================
  Coverage   93.73%   93.73%           
=======================================
  Files          78       78           
  Lines       11357    11357           
  Branches      656      656           
=======================================
+ Hits        10645    10646    +1     
+ Misses        642      641    -1     
  Partials       70       70           

Flag	Coverage Δ
go	91.17% <ø> (+0.05%)	⬆️
python	92.08% <ø> (ø)
rust	94.29% <ø> (ø)
typescript	96.56% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.