lan17 · Oct 15, 2026 · Oct 15, 2026 · Oct 15, 2026
@@ -38,7 +38,7 @@ on a port's replay report. Each port's mutation catalog defines its measured sco
 `make ci NODE22_BIN=/path/to/node22/bin/node` runs the complete pipeline,
 including integrations, mutations and the exact Node 22.15.0 package floor.
 See the repository's
-[formal guide](https://github.com/lan17/DialCache/blob/main/formal/README.md#generating-and-replaying-behavior)
+[formal guide](https://github.com/lan17/DialCache/blob/main/formal/README.md#run-it)
 for setup, reports and single-history reproduction.
 
 Pull requests run fast native/smoke checks and real integrations. Changes to

@@ -217,7 +217,7 @@
     },
     {
       "path": "docs/maintainers.md",
-      "sha256": "836a026530b6773e06aa461a29891fe8c6d2578360f5678702e8d7374d2deb09",
+      "sha256": "51b0808c1983de972421a15994bf1090bd20ca3a832a28d1a88dfc5ccc29951d",
       "entries": [
         {"title":"Maintainer guide","contracts":["B01"]},
         {"title":"Validation","contracts":["B01"]},
@@ -1084,16 +1084,21 @@
   "reviewedGuides": [
     {
       "path": "formal/README.md",
-      "sha256": "f03253dbdc8b87c8b272b16a0b0898413efddf9cb97a144b261810eff09633bc",
+      "sha256": "d37b38c1cdf72dbbf26eef1702136076354309bb4d1c497ddc39569b9b9b1578",
       "entries": [
         {"title":"Executable DialCache specification"},
         {"title":"Start with your task"},
+        {"title":"The setup, top to bottom"},
+        {"title":"1. State the rule in Quint"},
+        {"title":"2. Check the models"},
+        {"title":"3. Generate the corpus and the committed artifacts"},
+        {"title":"4. Replay every history in every port"},
+        {"title":"5. Account for the evidence"},
+        {"title":"6. Gate a change"},
+        {"title":"Pipelines"},
         {"title":"Where things are"},
-        {"title":"How the specification connects to code"},
-        {"title":"Models and composition profiles"},
-        {"title":"Generating and replaying behavior"},
-        {"title":"Shared verification and replay rules"},
-        {"title":"Evidence and scope"}
+        {"title":"Run it"},
+        {"title":"Reference"}
       ],
       "review": {
         "kind": "tooling-guide",
@@ -1102,7 +1107,7 @@
     },
     {
       "path": "formal/guides/AUTHORING.md",
-      "sha256": "46ea31d30b5cfebfa6163dfad1ad33b770148bf147329bb5c0a93271d4806962",
+      "sha256": "baca2abd313c0bcccce5e95d384d1cce7d60982a12fe192fee7680f143acd7a7",
       "entries": [
         {"title":"Reading and extending the DialCache models"},
         {"title":"Reading a model"},
@@ -1124,7 +1129,7 @@
     },
     {
       "path": "formal/guides/BEHAVIOR.md",
-      "sha256": "7adc2ad8756d8df060b09c6d6c83c6d084e612c7b21afe2107029cb3c2ea2e99",
+      "sha256": "5d6cb8d7e779cb99e6a60f6ea553b524d49c7a42b79a74f912a90ff44c5bafe8",
       "entries": [
         {"title":"Portable behavioral scenarios and generated profiles"},
         {"title":"Scenario format"},
@@ -1220,7 +1225,7 @@
     },
     {
       "path": "formal/guides/CONFORMANCE.md",
-      "sha256": "fb1edc1c05e51a8b647fcb1fe91fd5c75f48f6aae4920892ae479884af67adc7",
+      "sha256": "3bc580b0ea32bd21e53f54ec78523afb59ebaf40f8396b7884b51d4a7b8ec898",
       "entries": [
         {"title":"Core behavioral conformance profile"},
         {"title":"Trace format and trust boundary"},
@@ -1370,7 +1375,7 @@
     },
     {
       "path": "formal/guides/GLOSSARY.md",
-      "sha256": "2e1ae3a35f4b2c525a144e9cd7f079994bd3ebffb3a737c5dd770bd7f5e39fe8",
+      "sha256": "3737909010fb573669e59ee574b1fabd37131021b9faec5b36ca02d81a590f82",
       "entries": [
         {"title":"Glossary"},
         {"title":"Specification and replay"},
@@ -1381,6 +1386,7 @@
         {"title":"Connection model"},
         {"title":"Smoke"},
         {"title":"Lane"},
+        {"title":"ITF (Informal Trace Format)"},
         {"title":"Corpus, history, regression, exported run and public-only run"},
         {"title":"Differential"},
         {"title":"Bytes per state"},
@@ -1429,7 +1435,7 @@
     },
     {
       "path": "formal/guides/GO-PARITY.md",
-      "sha256": "1af6d885ef3490badfe7bc05f215bc20c3fad84bd9a2786ac4b62c00ce35e8c7",
+      "sha256": "956b12eabff3716bac5f4c57d14315c792dc89524c224a261fd15508992ff63f",
       "entries": [
         {"title":"Go parity acceptance"},
         {"title":"Required evidence"},
@@ -1475,7 +1481,7 @@
     },
     {
       "path": "formal/guides/PORTING.md",
-      "sha256": "22d0c0dc6ad513ee29f7008a83d8152ea77d1fff5a72c8393a643e0e71d5fe06",
+      "sha256": "342cfd680eeba31a57c7cc790693fb21d56e358e20ce105a6a6ce28a9e511a7e",
       "entries": [
         {"title":"Implementing another DialCache port"},
         {"title":"What a port supplies"},
@@ -1550,7 +1556,7 @@
     },
     {
       "path": "formal/guides/SEMANTIC-COVERAGE.md",
-      "sha256": "2834da3082acbcb70afffb4b4c18e5547209c47129f1ba681a598ac614d41539",
+      "sha256": "aaa54bdb961436a615dd4a0c1e29270c0c6ebe69adb24a41f97a0f26698e8282",
       "entries": [
         {"title":"Measuring semantic coverage"},
         {"title":"Evidence inventory"},
@@ -1673,7 +1679,7 @@
     },
     {
       "path": "formal/guides/TEST-MAP.md",
-      "sha256": "a32e4513667d38236aeb4df0b8c872912e725f1ae1605a6a91c07cb2970dc4d5",
+      "sha256": "66593388b326cd3c6b5378a1f98dc0cad28a2f39b387cc9b5efa032a28b0ec26",
       "entries": [
         {"title":"Formal contract and implementation evidence map"},
         {"title":"Behavioral map"},
@@ -1689,11 +1695,13 @@
     },
     {
       "path": "formal/guides/VALIDATION.md",
-      "sha256": "20132bd3ea23510eef25022fec91482fd09bf24f0a285f72aa018d69a69bd154",
+      "sha256": "f0dd128820f79d911cd086f9cbb523f7c3016304d9d3e9364e458aa62ca4fa2c",
       "entries": [
         {"title":"Validation and evidence"},
+        {"title":"Prerequisites"},
         {"title":"Choosing a run"},
         {"title":"Reading a completion report"},
+        {"title":"Reproducing one history"},
         {"title":"Mutation evidence"},
         {"title":"Exploratory runs"},
         {"title":"A retained sampling regression"}
@@ -1705,7 +1713,7 @@
     },
     {
       "path": "formal/guides/WALKTHROUGH.md",
-      "sha256": "c7d3bdb1e65f3672f94c61c5a5cccaf9f2bfd061f5de3f226dfa93973f4fab59",
+      "sha256": "17eb27c78c4be73e47cec8e08a8f33cf07d8f33116ab0e531f19f0f59f082174",
       "entries": [
         {"title":"Follow one behavior from Quint to every port"},
         {"title":"Read the named run first"},
@@ -1720,7 +1728,7 @@
     },
     {
       "path": "go/README.md",
-      "sha256": "97ceca7d13bc270a4e53341ce1d33b0a8f3906d4b4f26b7d2d30a8747f59f0f1",
+      "sha256": "fa465c2a7e53b4fe3ea2045708510c81ea5304e62533f99726d9bcdf1ba9c079",
       "entries": [
         {"title":"DialCache for Go"},
         {"title":"Use"},

@@ -27,7 +27,7 @@ ownership records. [Verification models](./GLOSSARY.md#verification-model) and [
 definitions. [Connection models](./GLOSSARY.md#connection-model) check selected profile histories against the
 acquired contracts. Conformance profiles also expose external actions that a
 language [driver](./GLOSSARY.md#driver) can replay. The
-[model inventory](../README.md#models-and-composition-profiles) and [profile registry](../catalogs/profiles.json)
+[model inventory](../models/README.md) and [profile registry](../catalogs/profiles.json)
 identify the relevant starting point. The words the models and guides share
 (driver, profile, flight, source, judgment, variant, witness and the rest) are
 defined in [GLOSSARY.md](./GLOSSARY.md), each with the file that owns it.
@@ -394,7 +394,7 @@ source expression moves or changes; its failure must never count as detection.
 
 For a model refactor, run the scheduled model checks/regressions, generation,
 implementation replay, evidence validation, and relevant mutation gates using
-the [documented commands](../README.md#generating-and-replaying-behavior). Keep the
+the [documented commands](../README.md#run-it). Keep the
 committed [smoke](./GLOSSARY.md#smoke) expectations unchanged. Compare pre/post generated action and
 state histories when preserving a fixed seed and schedule is intended, and
 investigate differences rather than replacing expectations to obtain a pass.

@@ -12,7 +12,7 @@ required witnesses in both languages. Fast PR checks use committed smoke,
 fixed supplements and freshness audits without claiming full parity;
 model/generator changes additionally recompute committed artifacts. Full
 validation remains required for behavior/model changes before merge and for
-release/new-port acceptance. See the [Make targets](../README.md#generating-and-replaying-behavior).
+release/new-port acceptance. See the [Make targets](../README.md#run-it).
 
 ## Scenario format
 
@@ -113,7 +113,7 @@ profile leaves to others, and how to replay a generated trace.
 
 ### Trace contract
 
-Each ITF state carries the authoritative `input.name` and `input.choice` beside the
+Each [ITF](./GLOSSARY.md#itf-informal-trace-format) state carries the authoritative `input.name` and `input.choice` beside the
 expected state `s`. The choice is a nonnegative ITF integer on actions that have
 choices and `-1` otherwise; optional `mbt::actionTaken` and `mbt::nondetPicks.choice`
 annotations must agree with it, and raw regression exports carry no annotations

@@ -4,7 +4,7 @@ This document specifies the bounded `core` profile implemented by the TypeScript
 
 ## Trace format and trust boundary
 
-Inputs use Quint 0.32.0's ITF JSON format. Each entry in `states` has:
+Inputs are Quint 0.32.0 [ITF](./GLOSSARY.md#itf-informal-trace-format) traces (the Informal Trace Format, JSON). Each entry in `states` has:
 
 - `input`: the authoritative public action, encoded as `{"name":"init","choice":{"#bigint":"-1"}}`. The first action is `init`; every core action uses `choice: -1` because it has no external arguments.
 - `s`: the expected model state after that action. Integers are encoded as `{"#bigint":"123"}`; booleans are JSON booleans.

@@ -39,9 +39,13 @@ One committed named history per conformance profile, `formal/generated/<profile>
 
 One validation pipeline run as its own make target and hosted CI job: the Quint evidence lane (`formal-check`), generation (`formal-generate`), the per-port parity lanes (`formal-ts`, `formal-go`, `formal-rust`, `formal-python`), the mutation lanes, and the differential, symbolic, exploration, smoke, audit and integration lanes. Parity and mutation lanes depend only on the generated corpus and witness evidence, so they run in parallel; the aggregate requires every lane. Owner: [VALIDATION.md](./VALIDATION.md)
 
+### ITF (Informal Trace Format)
+
+The JSON trace format Quint and Apalache write, defined by Informal Systems in [ADR-015](https://apalache-mc.org/docs/adr/015adr-trace.html) and produced by `quint run --out-itf` ([Quint CLI](https://quint.sh/docs/quint)). A trace is one object: a `#meta` header, the `vars` list and a `states` array holding one record of every variable per step. Integers are decimal strings inside `{"#bigint":"…"}` so no value loses precision; sets, tuples and maps use `#set`, `#tup` and `#map` wrappers. Every history here is one ITF file (`.itf.json`): the committed smoke traces, the sampled corpus and the exported regressions, each carrying the `mbt::actionTaken` and `mbt::nondetPicks` annotations the simulator adds beside the authoritative `input` record. The coordinator reads them through [itf.mjs](../replay/itf.mjs), which rejects an integer that would not survive as a JavaScript number. Owner: [itf.mjs](../replay/itf.mjs)
+
 ### Corpus, history, regression, exported run and public-only run
 
-A history is one ITF trace: an initial state then public actions, each recording its command in `input`. The corpus is everything a port replays: the sampled histories generation emits per profile plus the exported regressions. A regression is any `run ...Test` a scheduled model declares; a profile's public-only runs, whose every transition records a command, are exported for replay, while state-patching runs stay model-only. Owner: [AUTHORING.md](./AUTHORING.md), [execution.mjs](../tools/execution.mjs)
+A history is one [ITF](#itf-informal-trace-format) trace: an initial state then public actions, each recording its command in `input`. The corpus is everything a port replays: the sampled histories generation emits per profile plus the exported regressions. A regression is any `run ...Test` a scheduled model declares; a profile's public-only runs, whose every transition records a command, are exported for replay, while state-patching runs stay model-only. Owner: [AUTHORING.md](./AUTHORING.md), [execution.mjs](../tools/execution.mjs)
 
 ### Differential
 

@@ -29,7 +29,7 @@ artifact generation and prepared TS/Go replay. Run `make model-check` for the
 separate finite symbolic checks, then `make mutations` and `make integration`
 for their fault and real-server evidence.
 `make ci NODE22_BIN=/path/to/node22/bin/node` runs all local lanes in order,
-including symbolic checks and the exact Node 22.15.0 package floor; see the [Make target guide](../README.md#generating-and-replaying-behavior)
+including symbolic checks and the exact Node 22.15.0 package floor; see the [Make target guide](../README.md#run-it)
 for pinned prerequisites and individual targets.
 
 Hosted PR checks run native/race tests, committed smoke, audits and real

@@ -95,7 +95,8 @@ of the Go cache library.
 
 ## Trace and observation contract
 
-Quint exports ITF JSON. A trace contains a nonempty `states` array with an
+Quint exports [ITF](./GLOSSARY.md#itf-informal-trace-format) JSON, the Informal
+Trace Format. A trace contains a nonempty `states` array with an
 initial state followed by public actions. Reject unknown profiles/versions,
 unknown actions, malformed or out-of-domain choices, missing observations,
 misplaced initialization, and empty histories.
@@ -329,7 +330,7 @@ harness; those corruptions receive no positive conformance credit.
 
 ## Complete corpus and reusable acceptance checks
 
-Use the [shared Make targets and pinned prerequisites](../README.md#generating-and-replaying-behavior)
+Use the [shared Make targets and pinned prerequisites](../README.md#run-it)
 from the repository root:
 
 ```sh

@@ -85,7 +85,7 @@ histories against those records.
 | Exported boundary regressions | The exact public command sequence is checked in Quint and against both implementations |
 
 `make model-check` runs the symbolic checks declared in `execution.json` through
-checksummed standalone Apalache; see the [tool prerequisites](../README.md#generating-and-replaying-behavior).
+checksummed standalone Apalache; see the [tool prerequisites](./VALIDATION.md#prerequisites).
 This lane is separate from `make formal` and included in `make ci`.
 The model-property challenge catalog is the `challenges` array of
 [execution.json](../catalogs/execution.json). It runs once at the end of the scheduled
@@ -158,7 +158,7 @@ results; fresh measurements belong with their exact source and corpus artifacts.
 
 ## Reproduction and CI
 
-Use the [shared Make targets and pinned prerequisites](../README.md#generating-and-replaying-behavior):
+Use the [shared Make targets and pinned prerequisites](../README.md#run-it):
 
 ```sh
 make formal        # Regenerate and complete prepared TS, Go and Rust replay.

@@ -107,7 +107,7 @@ small compression caps exercise wrapper decisions without allocating the real
 
 ## Evidence and measurement
 
-Run the commands in [README.md](../README.md#generating-and-replaying-behavior)
+Run the commands in [README.md](../README.md#run-it)
 and inspect `node formal/tools/check-semantic-coverage.mjs` for current accounting.
 Checking a model, reaching a witness and replaying its observations are separate
 requirements. Both implementation completion gates derive the exact sampled