From c4b4aa9edb82f14cf7141c985b17cea8058133e3 Mon Sep 17 00:00:00 2001
From: Lev Neiman <lev.neiman@repl.it>
Date: Wed, 14 Oct 2026 17:58:05 -0700
Subject: [PATCH 1/2] feat(formal): measure Quint style and enforce two caps

`node formal/tools/check-style.mjs --report` prints the readability
measurements lan17/DialCache#220 tracks, from the sources, so progress
is reproducible: lines over 120 characters by area, module header
lengths, comment and guide sentence lengths, definitions with six or
more parameters or two adjacent booleans, and the free-text exclusion
reasons in execution.json. Today: 658 long lines (171 models, 180
kernel, 307 fixtures), longest header 25, 247 of 1,719 comment sentences
over 40 words, 93 of 2,221 guide sentences, 54 wide definitions, 5 with
adjacent booleans, 531 free-text exclusion reasons.

Without arguments it enforces the two rules guidance alone did not hold:
a Quint line is at most 120 characters and a module header at most 25
comment lines, over every file under formal/models not named for that
rule in formal/catalogs/style-allowlist.json. The allowlist names the 60
files that break the line cap today and no file for the header cap; it
carries no counts and only shrinks, because an entry whose file is clean
fails the check. The check is a step of `make audit`.

AUTHORING.md states the two caps beside the conventions they enforce;
the catalogs and tools indexes name the allowlist and the tool. Tests
cover the fake-tree cases (unlisted offender, stale entry, missing file,
header counting, report shape) and the committed tree.
---
 formal/catalogs/README.md            |   1 +
 formal/catalogs/source-audit.json    |   2 +-
 formal/catalogs/style-allowlist.json |  65 +++++++++++++
 formal/guides/AUTHORING.md           |  10 +-
 formal/tools/README.md               |   1 +
 formal/tools/check-style.mjs         | 131 +++++++++++++++++++++++++++
 formal/tools/validation.mjs          |   3 +-
 typescript/test/formal-style.test.ts |  72 +++++++++++++++
 8 files changed, 282 insertions(+), 3 deletions(-)
 create mode 100644 formal/catalogs/style-allowlist.json
 create mode 100644 formal/tools/check-style.mjs
 create mode 100644 typescript/test/formal-style.test.ts

diff --git a/formal/catalogs/README.md b/formal/catalogs/README.md
index 14d37151..2856e34b 100644
--- a/formal/catalogs/README.md
+++ b/formal/catalogs/README.md
@@ -26,6 +26,7 @@ output lives in [../generated/](../generated/README.md), never here.
 - [go-parity.json](./go-parity.json): the Go parity ledger over the catalogs, sources and audit; `check-go-parity.mjs`; its catalog, audit-dispositions and vector artifact digests re-pinned with `check-go-parity.mjs --refresh-inputs`, its mapping hashes by hand with the review.
 - [profile-lint-baseline.json](./profile-lint-baseline.json): the composition lint ratchet per profile; `node formal/tools/lint-profiles.mjs baseline --check`; `--write` after a reviewed fall.
 - [witness-baseline.json](./witness-baseline.json): the recorded witness hit counts the exploration gate compares against; `witnesses.mjs`; `baseline --write`.
+- [style-allowlist.json](./style-allowlist.json): the Quint files exempt from a style cap (line length, header length) because they broke it when the cap landed; `check-style.mjs`; shrinks only, by deleting a file's entry once it is clean.
 
 ## Fixed vector corpora
 
diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json
index 7cb31144..f3876235 100644
--- a/formal/catalogs/source-audit.json
+++ b/formal/catalogs/source-audit.json
@@ -1102,7 +1102,7 @@
     },
     {
       "path": "formal/guides/AUTHORING.md",
-      "sha256": "75ad1133cd6df5c50f9d4602022a92fb06281ea152b3dae43a60886a4b721489",
+      "sha256": "ecbfe0483a91ab2bf2c40db82dece7546cb764650abdf1bfc38cefa45be85343",
       "entries": [
         {"title":"Reading and extending the DialCache models"},
         {"title":"Reading a model"},
diff --git a/formal/catalogs/style-allowlist.json b/formal/catalogs/style-allowlist.json
new file mode 100644
index 00000000..e9784ffd
--- /dev/null
+++ b/formal/catalogs/style-allowlist.json
@@ -0,0 +1,65 @@
+{
+  "lineLength": [
+    "formal/models/dialcache-admission-conformance.qnt",
+    "formal/models/dialcache-core.qnt",
+    "formal/models/dialcache-dark-layers-conformance.qnt",
+    "formal/models/dialcache-effects-conformance.qnt",
+    "formal/models/dialcache-envelope-vectors.qnt",
+    "formal/models/dialcache-frame-vectors.qnt",
+    "formal/models/dialcache-independent-conformance.qnt",
+    "formal/models/dialcache-independent-connection.qnt",
+    "formal/models/dialcache-invalidation-transition.qnt",
+    "formal/models/dialcache-key-protocol.qnt",
+    "formal/models/dialcache-layers-conformance.qnt",
+    "formal/models/dialcache-local-clock-conformance.qnt",
+    "formal/models/dialcache-local-failure-conformance.qnt",
+    "formal/models/dialcache-policy-conformance.qnt",
+    "formal/models/dialcache-recovery-conformance.qnt",
+    "formal/models/dialcache-recovery-connection.qnt",
+    "formal/models/dialcache-recovery-read-conformance.qnt",
+    "formal/models/dialcache-recovery-read-connection.qnt",
+    "formal/models/dialcache-runtime-boundaries-conformance.qnt",
+    "formal/models/dialcache-runtime-policy.qnt",
+    "formal/models/dialcache-scope-conformance.qnt",
+    "formal/models/dialcache-shadow-conformance.qnt",
+    "formal/models/dialcache-shadow-layers-conformance.qnt",
+    "formal/models/dialcache-shadow-read-deadlines-conformance.qnt",
+    "formal/models/dialcache-source-budgets-conformance.qnt",
+    "formal/models/dialcache-stale-recovery.qnt",
+    "formal/models/fixtures/kernel/budgeted-local.qnt",
+    "formal/models/fixtures/kernel/fractional-clock.qnt",
+    "formal/models/fixtures/kernel/frame-clocks.qnt",
+    "formal/models/fixtures/kernel/frames-and-faults.qnt",
+    "formal/models/fixtures/kernel/held-dark-shadow.qnt",
+    "formal/models/fixtures/kernel/held-diagnostics.qnt",
+    "formal/models/fixtures/kernel/held-remote.qnt",
+    "formal/models/fixtures/kernel/held-replies.qnt",
+    "formal/models/fixtures/kernel/held-shadow.qnt",
+    "formal/models/fixtures/kernel/held-writes.qnt",
+    "formal/models/fixtures/kernel/local-faults.qnt",
+    "formal/models/fixtures/kernel/local-projection.qnt",
+    "formal/models/fixtures/kernel/markers.qnt",
+    "formal/models/fixtures/kernel/payload-classes.qnt",
+    "formal/models/fixtures/kernel/request-only.qnt",
+    "formal/models/fixtures/kernel/shadow-jobs.qnt",
+    "formal/models/kernel/adapter-replies.qnt",
+    "formal/models/kernel/compression.qnt",
+    "formal/models/kernel/deadlines.qnt",
+    "formal/models/kernel/diagnostics.qnt",
+    "formal/models/kernel/flights.qnt",
+    "formal/models/kernel/local-faults.qnt",
+    "formal/models/kernel/local-grid.qnt",
+    "formal/models/kernel/local-storage.qnt",
+    "formal/models/kernel/metrics.qnt",
+    "formal/models/kernel/payloads.qnt",
+    "formal/models/kernel/receipts.qnt",
+    "formal/models/kernel/recovery.qnt",
+    "formal/models/kernel/remote-frames.qnt",
+    "formal/models/kernel/remote-io.qnt",
+    "formal/models/kernel/remote-writes.qnt",
+    "formal/models/kernel/serving.qnt",
+    "formal/models/kernel/shadow-reads.qnt",
+    "formal/models/kernel/shadow.qnt"
+  ],
+  "headerLength": []
+}
diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md
index 0ba0db8c..6cfa3105 100644
--- a/formal/guides/AUTHORING.md
+++ b/formal/guides/AUTHORING.md
@@ -78,7 +78,15 @@ scrolling. Keep a genuinely short action compact. Prefer a descriptive
 intermediate state such as `published` or `completed` over a chain of `x`, `y`,
 and `z`. Comments should explain ownership, ordering, assumptions, or a boundary
 case, rather than narrate the syntax. Quint 0.32.0 has no CLI formatting command;
-these are reviewed authoring conventions.
+these are reviewed authoring conventions, with two of them enforced:
+`node formal/tools/check-style.mjs`, a step of `make audit`, fails a Quint line over
+120 characters and a module header over 25 comment lines in any file not named in
+[style-allowlist.json](../catalogs/style-allowlist.json). That list names the files
+that broke a cap when it landed and only shrinks: once a file is clean, delete its
+entry, or the check fails on the stale entry. `--report` prints the readability
+measurements (long lines, header lengths, comment and guide sentence lengths,
+parameter widths, free-text exclusion reasons) so progress is reproducible; those
+are reported, not enforced.
 
 A kernel module under `formal/models/kernel/` opens with one header of at most
 25 comment lines, each within 100 columns, in a fixed shape: one sentence of
diff --git a/formal/tools/README.md b/formal/tools/README.md
index 3ce7ca0b..c085a9f2 100644
--- a/formal/tools/README.md
+++ b/formal/tools/README.md
@@ -24,6 +24,7 @@ which scripts a target runs.
 - [check-symbolic-models.mjs](./check-symbolic-models.mjs): the finite symbolic checks with Apalache (`make model-check`).
 - [check-go-replay.mjs](./check-go-replay.mjs), [check-rust-replay.mjs](./check-rust-replay.mjs), [check-python-replay.mjs](./check-python-replay.mjs): each port's completion report against the required inventory.
 - [lint-profiles.mjs](./lint-profiles.mjs): the composition and witness-isolation lint over Quint's parsed IR; `baseline --check` ratchets.
+- [check-style.mjs](./check-style.mjs): the two Quint style caps (lines at most 120 characters, module headers at most 25 comment lines) over files not in the style allowlist; `--report` prints the readability measurements.
 - [differential.mjs](./differential.mjs): replays a composed profile's corpus against its reference revision in both directions (`make differential`).
 
 ## Generators (`make formal-generate`, `make fixtures-check`)
diff --git a/formal/tools/check-style.mjs b/formal/tools/check-style.mjs
new file mode 100644
index 00000000..d2aefea9
--- /dev/null
+++ b/formal/tools/check-style.mjs
@@ -0,0 +1,131 @@
+// Style measurements and two mechanical caps for the Quint sources.
+//
+// `--report` prints the measurement table lan17/DialCache#220 tracks, so
+// progress is reproducible: lines over 120 characters, module header
+// lengths, comment and guide sentence lengths, parameter widths and the
+// free-text exclusion reasons. Those are reported only; the editorial
+// guidance for them is AUTHORING.md "Writing conventions".
+//
+// Without arguments two rules are enforced, because guidance alone did not
+// hold for them: a Quint line is at most 120 characters and a module header
+// (the comment block between the `module` line and the first import or
+// definition) is at most 25 lines. Enforcement is over the files not named in
+// formal/catalogs/style-allowlist.json. The allowlist names today's
+// offenders per rule and carries no counts; a file that becomes clean must be
+// deleted from it (a stale entry fails the check), so the list only shrinks.
+import { readFileSync, readdirSync } from 'node:fs';
+import { resolve } from 'node:path';
+import { fileURLToPath } from 'node:url';
+
+export const root = fileURLToPath(new URL('../../', import.meta.url));
+export const allowlistPath = 'formal/catalogs/style-allowlist.json';
+export const caps = { lineLength: 120, headerLength: 25 };
+const read = (path, directory) => readFileSync(resolve(directory, path), 'utf8');
+
+export function quintFiles(directory = root) {
+  const walk = relative => readdirSync(resolve(directory, relative), { withFileTypes: true }).flatMap(entry =>
+    entry.isDirectory() ? walk(`${relative}/${entry.name}`) : entry.name.endsWith('.qnt') ? [`${relative}/${entry.name}`] : []);
+  return walk('formal/models').sort();
+}
+
+// The header: comment lines after the `module` line, up to the first line
+// that is neither blank nor a comment.
+export function headerLines(lines) {
+  const start = lines.findIndex(line => /^\s*module\s+\w+/.test(line));
+  if (start < 0) return 0;
+  let count = 0;
+  for (const line of lines.slice(start + 1)) {
+    const trimmed = line.trim();
+    if (trimmed.startsWith('//')) count++;
+    else if (trimmed !== '') break;
+  }
+  return count;
+}
+
+const sentences = text => text.split(/(?<=[.!?])\s+(?=[A-Z`\[(])/).map(s => s.split(/\s+/).filter(Boolean).length).filter(Boolean);
+
+export function measure(directory = root) {
+  const files = quintFiles(directory);
+  const areas = { models: 0, kernel: 0, fixtures: 0 };
+  let longLines = 0, headerTotal = 0, headerMax = 0, headersOver = 0, definitions = 0, wide = 0;
+  const twoBooleans = [];
+  const commentWords = [];
+  for (const path of files) {
+    const text = read(path, directory);
+    const lines = text.split('\n');
+    const over = lines.filter(line => line.length > caps.lineLength).length;
+    longLines += over;
+    areas[path.includes('/fixtures/') ? 'fixtures' : path.includes('/kernel/') ? 'kernel' : 'models'] += over;
+    const header = headerLines(lines);
+    headerTotal += header; headerMax = Math.max(headerMax, header); headersOver += header > caps.headerLength;
+    commentWords.push(...sentences(lines.filter(line => line.trim().startsWith('//')).map(line => line.trim().replace(/^\/\/\s?/, '')).join(' ')));
+    for (const match of text.matchAll(/\b(?:pure )?def\s+(\w+)\s*\(([^)]*)\)/g)) {
+      definitions++;
+      const params = match[2].split(',').map(p => p.trim()).filter(Boolean);
+      if (params.length >= 6) wide++;
+      const types = params.map(p => p.split(':').at(-1).trim());
+      if (types.some((type, i) => type === 'bool' && types[i + 1] === 'bool')) twoBooleans.push(`${path.split('/').pop()}:${match[1]}`);
+    }
+  }
+  const guideWords = [];
+  for (const path of [...readdirSync(resolve(directory, 'formal/guides')).filter(p => p.endsWith('.md')).map(p => `formal/guides/${p}`), 'formal/README.md']) {
+    const text = read(path, directory).replace(/```[\s\S]*?```/g, '');
+    for (const paragraph of text.split(/\n\s*\n/)) {
+      if (/^\s*[#|]/.test(paragraph)) continue;
+      guideWords.push(...sentences(paragraph.split('\n').map(line => line.trim()).join(' ')));
+    }
+  }
+  const execution = JSON.parse(read('formal/catalogs/execution.json', directory));
+  const exclusionReasons = (execution.challenges ?? []).reduce((count, challenge) => count + Object.values(challenge.reproducer?.exclusions ?? {}).filter(value => typeof value === 'string').length, 0);
+  const average = values => values.length ? Math.round(values.reduce((a, b) => a + b, 0) / values.length * 10) / 10 : 0;
+  return {
+    files: files.length,
+    linesOver: { total: longLines, ...areas },
+    headers: { total: headerTotal, longest: headerMax, overCap: headersOver },
+    commentSentences: { count: commentWords.length, over40: commentWords.filter(w => w > 40).length, averageWords: average(commentWords) },
+    guideSentences: { count: guideWords.length, over40: guideWords.filter(w => w > 40).length },
+    definitions: { count: definitions, sixOrMoreParameters: wide, twoAdjacentBooleans: twoBooleans },
+    exclusionReasons,
+  };
+}
+
+export function renderReport(m) {
+  return [
+    '| Measure | Value |', '| --- | --- |',
+    `| Quint files under formal/models | ${m.files} |`,
+    `| Lines over ${caps.lineLength} characters (models / kernel / fixtures) | ${m.linesOver.total} (${m.linesOver.models} / ${m.linesOver.kernel} / ${m.linesOver.fixtures}) |`,
+    `| Module header comment lines, total / longest / over ${caps.headerLength} | ${m.headers.total} / ${m.headers.longest} / ${m.headers.overCap} |`,
+    `| Quint comment sentences, count / over 40 words / average words | ${m.commentSentences.count} / ${m.commentSentences.over40} / ${m.commentSentences.averageWords} |`,
+    `| Guide sentences, count / over 40 words | ${m.guideSentences.count} / ${m.guideSentences.over40} |`,
+    `| Definitions, count / six or more parameters / two adjacent booleans | ${m.definitions.count} / ${m.definitions.sixOrMoreParameters} / ${m.definitions.twoAdjacentBooleans.length} (${m.definitions.twoAdjacentBooleans.join(', ') || 'none'}) |`,
+    `| Free-text exclusion reasons in execution.json | ${m.exclusionReasons} |`,
+  ].join('\n') + '\n';
+}
+
+// The two caps over every file not allowlisted for that rule; an allowlisted
+// file that is clean is reported too, so the list only ever shrinks.
+export function checkStyle({ directory = root, allowlist = JSON.parse(read(allowlistPath, directory)) } = {}) {
+  const failures = [];
+  const listed = { lineLength: new Set(allowlist.lineLength ?? []), headerLength: new Set(allowlist.headerLength ?? []) };
+  const files = quintFiles(directory);
+  for (const rule of Object.keys(listed)) for (const path of listed[rule]) if (!files.includes(path)) failures.push(`${allowlistPath}: ${rule} names a file that does not exist: ${path}`);
+  let checked = 0;
+  for (const path of files) {
+    const lines = read(path, directory).split('\n');
+    const long = lines.map((line, index) => line.length > caps.lineLength ? index + 1 : 0).filter(Boolean);
+    const header = headerLines(lines);
+    if (listed.lineLength.has(path)) { if (!long.length) failures.push(`${allowlistPath}: ${path} has no line over ${caps.lineLength}; delete its lineLength entry`); }
+    else { checked++; for (const line of long) failures.push(`${path}:${line}: line over ${caps.lineLength} characters`); }
+    if (listed.headerLength.has(path)) { if (header <= caps.headerLength) failures.push(`${allowlistPath}: ${path} has a header within ${caps.headerLength} lines; delete its headerLength entry`); }
+    else if (header > caps.headerLength) failures.push(`${path}: module header has ${header} comment lines (cap ${caps.headerLength})`);
+  }
+  if (failures.length) throw new Error(failures.join('\n'));
+  return { files: files.length, lineLengthChecked: checked, allowlisted: listed.lineLength.size + listed.headerLength.size };
+}
+
+if (process.argv[1] === fileURLToPath(import.meta.url)) {
+  const [flag] = process.argv.slice(2);
+  if (flag === '--report') process.stdout.write(renderReport(measure()));
+  else if (flag === undefined) console.log(checkStyle());
+  else { console.error('Usage: node formal/tools/check-style.mjs [--report]'); process.exitCode = 2; }
+}
diff --git a/formal/tools/validation.mjs b/formal/tools/validation.mjs
index 2271fb42..6b89c362 100644
--- a/formal/tools/validation.mjs
+++ b/formal/tools/validation.mjs
@@ -21,7 +21,7 @@ export const targetDescriptions = {
   'check-rust': 'Rust formatting check, clippy with warnings denied and default tests including the smoke conformance run',
   'check-python': 'Python native, protocol, scenario and committed smoke tests with coverage (coverage/python/native.lcov)',
   docs: 'Check shared examples and links; generate native API references and the documentation site (Go, Rust and Python required)',
-  audit: 'Check source, behavior, feature, Go and generated-fixture freshness inventories',
+  audit: 'Check source, behavior, feature, Go and generated-fixture freshness inventories and the Quint style caps',
   smoke: 'Replay committed Quint-derived fixtures in TypeScript, Go, Rust and Python; no full completion claim',
   formal: 'Check every scheduled Quint model, generate the complete corpus and shared witness evidence, then replay TypeScript, Go, Rust and Python',
   'formal-check': 'Typecheck and run every scheduled Quint model, its public regressions and the model mutation challenges',
@@ -195,6 +195,7 @@ export function validationPlan(target, { directory = root, environment = process
     audit: ['execution', 'check-source-audit', 'check-semantic-coverage', 'check-feature-coverage', 'check-go-parity']
       .map(name => node(`Check ${name}`, `formal/tools/${name}.mjs`))
       .concat(node('Verify committed fixture fingerprints', 'formal/tools/generated-fixtures.mjs', '--verify'),
+        node('Check the Quint style caps', 'formal/tools/check-style.mjs'),
         node('Check conditional fixture regeneration scope', '--test', '.github/scripts/fixture-scope.test.mjs')),
     smoke: [tsReplay(false), nativeGo(false), nativeRust(false),
       python('Replay committed Python fixtures and scenarios', '-m', 'pytest', 'python/tests/test_conformance.py')],
diff --git a/typescript/test/formal-style.test.ts b/typescript/test/formal-style.test.ts
new file mode 100644
index 00000000..c5c28b17
--- /dev/null
+++ b/typescript/test/formal-style.test.ts
@@ -0,0 +1,72 @@
+import { mkdirSync, mkdtempSync, rmSync, writeFileSync } from "node:fs";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { afterEach, beforeEach, describe, expect, it } from "vitest";
+
+const { checkStyle, measure, renderReport, headerLines, caps } = await import(
+  new URL("../../formal/tools/check-style.mjs", import.meta.url).href,
+) as {
+  checkStyle(options?: { directory?: string; allowlist?: { lineLength?: string[]; headerLength?: string[] } }): { files: number; lineLengthChecked: number; allowlisted: number };
+  measure(directory?: string): { files: number; linesOver: { total: number }; headers: { longest: number; overCap: number }; commentSentences: { over40: number }; definitions: { twoAdjacentBooleans: string[] }; exclusionReasons: number };
+  renderReport(measurements: unknown): string;
+  headerLines(lines: string[]): number;
+  caps: { lineLength: number; headerLength: number };
+};
+
+describe("Quint style caps", () => {
+  let directory: string;
+  const put = (path: string, text: string) => writeFileSync(join(directory, path), text);
+  const longLine = `  pure val wide = ${"1 + ".repeat(40)}1`;
+  const header = (lines: number) => ["module m {", ...Array.from({ length: lines }, (_, i) => `  // Header line ${i + 1}.`), "  pure val x = 1", "}", ""].join("\n");
+
+  beforeEach(() => {
+    directory = mkdtempSync(join(tmpdir(), "dialcache-style-"));
+    for (const path of ["formal/models/kernel", "formal/models/fixtures/kernel", "formal/guides", "formal/catalogs"]) mkdirSync(join(directory, path), { recursive: true });
+    put("formal/models/clean.qnt", header(3));
+    put("formal/models/kernel/tall.qnt", header(26));
+    put("formal/models/fixtures/kernel/wide.qnt", `module w {\n${longLine}\n}\n`);
+    put("formal/guides/GUIDE.md", "# Guide\n\nShort sentence. " + "word ".repeat(45) + "ends here.\n");
+    put("formal/README.md", "# Formal\n\nOne sentence.\n");
+    put("formal/catalogs/execution.json", JSON.stringify({ challenges: [{ reproducer: { exclusions: { a: "free text", b: { reason: "slug" } } } }] }));
+    put("formal/catalogs/style-allowlist.json", JSON.stringify({ lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: ["formal/models/kernel/tall.qnt"] }));
+  });
+  afterEach(() => rmSync(directory, { recursive: true, force: true }));
+
+  it("passes when every offender is allowlisted and counts what it checked", () => {
+    expect(checkStyle({ directory })).toEqual({ files: 3, lineLengthChecked: 2, allowlisted: 2 });
+  });
+
+  it("fails a long line and a tall header in files that are not allowlisted, naming the line", () => {
+    expect(() => checkStyle({ directory, allowlist: { lineLength: [], headerLength: ["formal/models/kernel/tall.qnt"] } }))
+      .toThrow(/^formal\/models\/fixtures\/kernel\/wide.qnt:2: line over 120 characters$/m);
+    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: [] } }))
+      .toThrow(/tall.qnt: module header has 26 comment lines \(cap 25\)/);
+  });
+
+  it("fails a stale allowlist entry so the list only shrinks, and a missing file", () => {
+    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt", "formal/models/clean.qnt"], headerLength: ["formal/models/kernel/tall.qnt"] } }))
+      .toThrow(/clean.qnt has no line over 120; delete its lineLength entry/);
+    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt", "formal/models/missing.qnt"], headerLength: ["formal/models/kernel/tall.qnt"] } }))
+      .toThrow(/names a file that does not exist: formal\/models\/missing.qnt/);
+  });
+
+  it("measures headers from the module line to the first non-comment line", () => {
+    expect(headerLines(["module m {", "  // a", "", "  // b", "  import x.* from \"./x\"", "  // not header", "}"])).toBe(2);
+    expect(headerLines(["// file comment", "module m {", "  pure val x = 1"])).toBe(0);
+  });
+
+  it("reports the measurements the readability plan tracks", () => {
+    const m = measure(directory);
+    expect(m).toMatchObject({ files: 3, linesOver: { total: 1, fixtures: 1 }, headers: { longest: 26, overCap: 1 }, exclusionReasons: 1 });
+    expect(m.commentSentences.over40).toBe(0);
+    const report = renderReport(m);
+    expect(report).toContain(`| Lines over ${caps.lineLength} characters (models / kernel / fixtures) | 1 (0 / 0 / 1) |`);
+    expect(report).toContain("| Free-text exclusion reasons in execution.json | 1 |");
+  });
+
+  it("holds on the committed tree: every current offender is allowlisted and no allowlist entry is stale", () => {
+    const result = checkStyle();
+    expect(result.files).toBeGreaterThan(50);
+    expect(measure().headers.overCap).toBe(0);
+  });
+});

From 7e7143d74e56b3c8a67268e8bfca1572fee13e14 Mon Sep 17 00:00:00 2001
From: Lev Neiman <lev.neiman@repl.it>
Date: Wed, 14 Oct 2026 18:25:37 -0700
Subject: [PATCH 2/2] fix(formal): count a header written before the module
 line; align the metrics with #220

Review follow-up on the style checker. The header cap counted only the
comment block after the `module` line, and every kernel fixture writes
its header before it: sixteen files scored zero and two
(held-remote.qnt, payload-classes.qnt) exceed the cap, which was also a
bypass. The header is now the comment block beside the `module` line on
either side, the two offenders are allowlisted for the header rule, and
the test pins the leading-block case and a stale header entry.

The comment-sentence metric no longer counts section banner lines as
sentence text (they glued neighbouring sentences into 98 of the 247
reported long ones), and both sentence rows report the over 40, 60 and
100 word counts, the longest and the average, as #220 tracked. The
boolean-parameter metric counts definitions with two or more boolean
parameters anywhere in the signature, actions included, with the
parameter list scanned to its matching parenthesis, so shadow::newJob,
one of C2's four targets, appears and an operator-typed parameter is one
parameter; the wide-definition count is given per area. The tool header
states every measurement's definition. AUTHORING defines the header,
names the scope and says the allowlist grows only as a reviewed
exception; the tools index heading names the audit lane correctly.
---
 formal/catalogs/README.md            |  2 +-
 formal/catalogs/source-audit.json    |  2 +-
 formal/catalogs/style-allowlist.json |  5 +-
 formal/guides/AUTHORING.md           | 19 ++++---
 formal/tools/README.md               |  7 ++-
 formal/tools/check-style.mjs         | 82 +++++++++++++++++++++-------
 typescript/test/formal-style.test.ts | 67 +++++++++++++++++------
 7 files changed, 136 insertions(+), 48 deletions(-)

diff --git a/formal/catalogs/README.md b/formal/catalogs/README.md
index 2856e34b..8c6d5127 100644
--- a/formal/catalogs/README.md
+++ b/formal/catalogs/README.md
@@ -26,7 +26,7 @@ output lives in [../generated/](../generated/README.md), never here.
 - [go-parity.json](./go-parity.json): the Go parity ledger over the catalogs, sources and audit; `check-go-parity.mjs`; its catalog, audit-dispositions and vector artifact digests re-pinned with `check-go-parity.mjs --refresh-inputs`, its mapping hashes by hand with the review.
 - [profile-lint-baseline.json](./profile-lint-baseline.json): the composition lint ratchet per profile; `node formal/tools/lint-profiles.mjs baseline --check`; `--write` after a reviewed fall.
 - [witness-baseline.json](./witness-baseline.json): the recorded witness hit counts the exploration gate compares against; `witnesses.mjs`; `baseline --write`.
-- [style-allowlist.json](./style-allowlist.json): the Quint files exempt from a style cap (line length, header length) because they broke it when the cap landed; `check-style.mjs`; shrinks only, by deleting a file's entry once it is clean.
+- [style-allowlist.json](./style-allowlist.json): the Quint files exempt from a style cap (line length, header length) because they broke it when the cap landed; `check-style.mjs`; a stale entry fails, so the list shrinks by deleting a file's entry once it is clean, and grows only as a reviewed exception.
 
 ## Fixed vector corpora
 
diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json
index f3876235..b4a7585b 100644
--- a/formal/catalogs/source-audit.json
+++ b/formal/catalogs/source-audit.json
@@ -1102,7 +1102,7 @@
     },
     {
       "path": "formal/guides/AUTHORING.md",
-      "sha256": "ecbfe0483a91ab2bf2c40db82dece7546cb764650abdf1bfc38cefa45be85343",
+      "sha256": "7f3aee31a1f311f27420550960f1ceed757ecae1f1616bea01436a9635cd12f6",
       "entries": [
         {"title":"Reading and extending the DialCache models"},
         {"title":"Reading a model"},
diff --git a/formal/catalogs/style-allowlist.json b/formal/catalogs/style-allowlist.json
index e9784ffd..99f953fe 100644
--- a/formal/catalogs/style-allowlist.json
+++ b/formal/catalogs/style-allowlist.json
@@ -61,5 +61,8 @@
     "formal/models/kernel/shadow-reads.qnt",
     "formal/models/kernel/shadow.qnt"
   ],
-  "headerLength": []
+  "headerLength": [
+    "formal/models/fixtures/kernel/held-remote.qnt",
+    "formal/models/fixtures/kernel/payload-classes.qnt"
+  ]
 }
diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md
index 6cfa3105..c8a4221a 100644
--- a/formal/guides/AUTHORING.md
+++ b/formal/guides/AUTHORING.md
@@ -78,15 +78,18 @@ scrolling. Keep a genuinely short action compact. Prefer a descriptive
 intermediate state such as `published` or `completed` over a chain of `x`, `y`,
 and `z`. Comments should explain ownership, ordering, assumptions, or a boundary
 case, rather than narrate the syntax. Quint 0.32.0 has no CLI formatting command;
-these are reviewed authoring conventions, with two of them enforced:
+these are reviewed authoring conventions, with two of them enforced.
 `node formal/tools/check-style.mjs`, a step of `make audit`, fails a Quint line over
-120 characters and a module header over 25 comment lines in any file not named in
-[style-allowlist.json](../catalogs/style-allowlist.json). That list names the files
-that broke a cap when it landed and only shrinks: once a file is clean, delete its
-entry, or the check fails on the stale entry. `--report` prints the readability
-measurements (long lines, header lengths, comment and guide sentence lengths,
-parameter widths, free-text exclusion reasons) so progress is reproducible; those
-are reported, not enforced.
+120 characters and a module header over 25 comment lines in any `.qnt` file under
+`formal/models` not named for that rule in
+[style-allowlist.json](../catalogs/style-allowlist.json). The header is the `//`
+comment block beside the `module` line, written before it or after it, up to the
+first import or definition. The allowlist names the files that broke a cap when it
+landed and may only shrink: once a file is clean, delete its entry, or the check
+fails on the stale entry; adding an entry is a reviewed exception. `--report`
+prints the readability measurements so progress is reproducible: long lines,
+header lengths, comment and guide sentence lengths, parameter widths and the
+free-text exclusion reasons. Those are reported, not enforced.
 
 A kernel module under `formal/models/kernel/` opens with one header of at most
 25 comment lines, each within 100 columns, in a fixed shape: one sentence of
diff --git a/formal/tools/README.md b/formal/tools/README.md
index c085a9f2..fc8a6365 100644
--- a/formal/tools/README.md
+++ b/formal/tools/README.md
@@ -13,18 +13,21 @@ which scripts a target runs.
 - [validation.mjs](./validation.mjs): the target dispatcher; composes every `make` target from the scripts below and checks prerequisites.
 - [execution.mjs](./execution.mjs): reads and validates the execution manifest; `node formal/tools/execution.mjs` prints the inventory.
 
-## Checks (the `audit` lane runs `execution.mjs` and the first four)
+## Checks
+
+The `audit` lane runs `execution.mjs`, the first five checks below and the
+generated-fixture verification; `validation.mjs` is the list of record.
 
 - [check-source-audit.mjs](./check-source-audit.mjs): the docs and test review ledger against the current files; `--refresh <path>...` re-keys the named files after their review.
 - [check-semantic-coverage.mjs](./check-semantic-coverage.mjs): every semantic case cites scheduled checks, scenarios, vectors and witnesses.
 - [check-feature-coverage.mjs](./check-feature-coverage.mjs): the native feature inventory and its evidence references.
 - [check-go-parity.mjs](./check-go-parity.mjs): the Go parity ledger against the catalogs and both source trees; `--refresh-inputs` re-pins its catalog, audit-dispositions and vector artifact digests.
+- [check-style.mjs](./check-style.mjs): the two Quint style caps (lines at most 120 characters, module headers at most 25 comment lines) over files not in the style allowlist; `--report` prints the readability measurements.
 - [check-model-properties.mjs](./check-model-properties.mjs): the model-fault challenge catalog; `--only=<id>` measures one.
 - [check-kernel-fixtures.mjs](./check-kernel-fixtures.mjs): typechecks and runs the kernel fixtures (`make kernel-fixtures`).
 - [check-symbolic-models.mjs](./check-symbolic-models.mjs): the finite symbolic checks with Apalache (`make model-check`).
 - [check-go-replay.mjs](./check-go-replay.mjs), [check-rust-replay.mjs](./check-rust-replay.mjs), [check-python-replay.mjs](./check-python-replay.mjs): each port's completion report against the required inventory.
 - [lint-profiles.mjs](./lint-profiles.mjs): the composition and witness-isolation lint over Quint's parsed IR; `baseline --check` ratchets.
-- [check-style.mjs](./check-style.mjs): the two Quint style caps (lines at most 120 characters, module headers at most 25 comment lines) over files not in the style allowlist; `--report` prints the readability measurements.
 - [differential.mjs](./differential.mjs): replays a composed profile's corpus against its reference revision in both directions (`make differential`).
 
 ## Generators (`make formal-generate`, `make fixtures-check`)
diff --git a/formal/tools/check-style.mjs b/formal/tools/check-style.mjs
index d2aefea9..cb3e4aa6 100644
--- a/formal/tools/check-style.mjs
+++ b/formal/tools/check-style.mjs
@@ -8,11 +8,24 @@
 //
 // Without arguments two rules are enforced, because guidance alone did not
 // hold for them: a Quint line is at most 120 characters and a module header
-// (the comment block between the `module` line and the first import or
-// definition) is at most 25 lines. Enforcement is over the files not named in
+// is at most 25 comment lines. The header is the `//` comment block beside
+// the `module` line: the contiguous comment lines directly above it plus the
+// comment lines below it up to the first import or definition (blank lines
+// between them allowed), so a header written before `module`, as the kernel
+// fixtures do, counts the same as one written after. Enforcement is over the
+// `.qnt` files under formal/models not named in
 // formal/catalogs/style-allowlist.json. The allowlist names today's
 // offenders per rule and carries no counts; a file that becomes clean must be
-// deleted from it (a stale entry fails the check), so the list only shrinks.
+// deleted from it (a stale entry fails the check), so the list may only
+// shrink, and adding an entry is a reviewed exception.
+//
+// Measurement definitions, so the report is reproducible: a comment sentence
+// is a run of full-line `//` comments joined by spaces, with banner lines
+// (dashes only, or a title between dashes) removed, split before a capital
+// letter, backtick, bracket or parenthesis that follows sentence punctuation;
+// a guide sentence is the same split over a paragraph outside headings, tables
+// and code fences; a definition is a `def`, `pure def` or `action` with its
+// parameter list scanned to the matching parenthesis.
 import { readFileSync, readdirSync } from 'node:fs';
 import { resolve } from 'node:path';
 import { fileURLToPath } from 'node:url';
@@ -34,6 +47,11 @@ export function headerLines(lines) {
   const start = lines.findIndex(line => /^\s*module\s+\w+/.test(line));
   if (start < 0) return 0;
   let count = 0;
+  for (let index = start - 1; index >= 0; index--) {
+    const trimmed = lines[index].trim();
+    if (trimmed.startsWith('//')) count++;
+    else if (trimmed !== '') break;
+  }
   for (const line of lines.slice(start + 1)) {
     const trimmed = line.trim();
     if (trimmed.startsWith('//')) count++;
@@ -42,12 +60,36 @@ export function headerLines(lines) {
   return count;
 }
 
+const isBanner = text => /^-{3,}/.test(text) || /^-{2,}\s.*\s-{2,}$/.test(text);
+
+// Every def, pure def and action with its parameters, the list scanned to the
+// matching parenthesis so an operator-typed parameter is one parameter.
+export function definitions(text) {
+  const found = [];
+  for (const match of text.matchAll(/\b(?:pure\s+)?(?:def|action)\s+(\w+)\s*\(/g)) {
+    let depth = 1, index = match.index + match[0].length, start = index;
+    const params = [];
+    for (; index < text.length && depth > 0; index++) {
+      const char = text[index];
+      if (char === '(' || char === '[') depth++;
+      else if (char === ')' || char === ']') { depth--; if (depth === 0) break; }
+      else if (char === ',' && depth === 1) { params.push(text.slice(start, index)); start = index + 1; }
+    }
+    const last = text.slice(start, index).trim();
+    if (last) params.push(last);
+    found.push({ name: match[1], params: params.map(param => param.trim()).filter(Boolean) });
+  }
+  return found;
+}
+
 const sentences = text => text.split(/(?<=[.!?])\s+(?=[A-Z`\[(])/).map(s => s.split(/\s+/).filter(Boolean).length).filter(Boolean);
+const area = path => path.includes('/fixtures/') ? 'fixtures' : path.includes('/kernel/') ? 'kernel' : 'models';
 
 export function measure(directory = root) {
   const files = quintFiles(directory);
   const areas = { models: 0, kernel: 0, fixtures: 0 };
-  let longLines = 0, headerTotal = 0, headerMax = 0, headersOver = 0, definitions = 0, wide = 0;
+  const wide = { models: 0, kernel: 0, fixtures: 0 };
+  let longLines = 0, headerTotal = 0, headerMax = 0, headersOver = 0, definitionCount = 0;
   const twoBooleans = [];
   const commentWords = [];
   for (const path of files) {
@@ -55,16 +97,16 @@ export function measure(directory = root) {
     const lines = text.split('\n');
     const over = lines.filter(line => line.length > caps.lineLength).length;
     longLines += over;
-    areas[path.includes('/fixtures/') ? 'fixtures' : path.includes('/kernel/') ? 'kernel' : 'models'] += over;
+    areas[area(path)] += over;
     const header = headerLines(lines);
     headerTotal += header; headerMax = Math.max(headerMax, header); headersOver += header > caps.headerLength;
-    commentWords.push(...sentences(lines.filter(line => line.trim().startsWith('//')).map(line => line.trim().replace(/^\/\/\s?/, '')).join(' ')));
-    for (const match of text.matchAll(/\b(?:pure )?def\s+(\w+)\s*\(([^)]*)\)/g)) {
-      definitions++;
-      const params = match[2].split(',').map(p => p.trim()).filter(Boolean);
-      if (params.length >= 6) wide++;
-      const types = params.map(p => p.split(':').at(-1).trim());
-      if (types.some((type, i) => type === 'bool' && types[i + 1] === 'bool')) twoBooleans.push(`${path.split('/').pop()}:${match[1]}`);
+    const comments = lines.filter(line => line.trim().startsWith('//')).map(line => line.trim().replace(/^\/\/\s?/, '')).filter(line => !isBanner(line));
+    commentWords.push(...sentences(comments.join(' ')));
+    for (const definition of definitions(text)) {
+      definitionCount++;
+      if (definition.params.length >= 6) wide[area(path)]++;
+      const booleans = definition.params.filter(param => param.split(':').at(-1).trim() === 'bool').length;
+      if (booleans >= 2) twoBooleans.push(`${path.replace(/^formal\/models\//, '')}:${definition.name}`);
     }
   }
   const guideWords = [];
@@ -78,13 +120,14 @@ export function measure(directory = root) {
   const execution = JSON.parse(read('formal/catalogs/execution.json', directory));
   const exclusionReasons = (execution.challenges ?? []).reduce((count, challenge) => count + Object.values(challenge.reproducer?.exclusions ?? {}).filter(value => typeof value === 'string').length, 0);
   const average = values => values.length ? Math.round(values.reduce((a, b) => a + b, 0) / values.length * 10) / 10 : 0;
+  const distribution = values => ({ count: values.length, over40: values.filter(w => w > 40).length, over60: values.filter(w => w > 60).length, over100: values.filter(w => w > 100).length, longest: Math.max(0, ...values), averageWords: average(values) });
   return {
     files: files.length,
     linesOver: { total: longLines, ...areas },
     headers: { total: headerTotal, longest: headerMax, overCap: headersOver },
-    commentSentences: { count: commentWords.length, over40: commentWords.filter(w => w > 40).length, averageWords: average(commentWords) },
-    guideSentences: { count: guideWords.length, over40: guideWords.filter(w => w > 40).length },
-    definitions: { count: definitions, sixOrMoreParameters: wide, twoAdjacentBooleans: twoBooleans },
+    commentSentences: distribution(commentWords),
+    guideSentences: distribution(guideWords),
+    definitions: { count: definitionCount, sixOrMoreParameters: wide, twoBooleanParameters: twoBooleans },
     exclusionReasons,
   };
 }
@@ -95,9 +138,10 @@ export function renderReport(m) {
     `| Quint files under formal/models | ${m.files} |`,
     `| Lines over ${caps.lineLength} characters (models / kernel / fixtures) | ${m.linesOver.total} (${m.linesOver.models} / ${m.linesOver.kernel} / ${m.linesOver.fixtures}) |`,
     `| Module header comment lines, total / longest / over ${caps.headerLength} | ${m.headers.total} / ${m.headers.longest} / ${m.headers.overCap} |`,
-    `| Quint comment sentences, count / over 40 words / average words | ${m.commentSentences.count} / ${m.commentSentences.over40} / ${m.commentSentences.averageWords} |`,
-    `| Guide sentences, count / over 40 words | ${m.guideSentences.count} / ${m.guideSentences.over40} |`,
-    `| Definitions, count / six or more parameters / two adjacent booleans | ${m.definitions.count} / ${m.definitions.sixOrMoreParameters} / ${m.definitions.twoAdjacentBooleans.length} (${m.definitions.twoAdjacentBooleans.join(', ') || 'none'}) |`,
+    `| Quint comment sentences, count / over 40 / over 60 / over 100 words / longest / average | ${m.commentSentences.count} / ${m.commentSentences.over40} / ${m.commentSentences.over60} / ${m.commentSentences.over100} / ${m.commentSentences.longest} / ${m.commentSentences.averageWords} |`,
+    `| Guide sentences, count / over 40 / over 60 / over 100 words / longest / average | ${m.guideSentences.count} / ${m.guideSentences.over40} / ${m.guideSentences.over60} / ${m.guideSentences.over100} / ${m.guideSentences.longest} / ${m.guideSentences.averageWords} |`,
+    `| Definitions, count / six or more parameters (models / kernel / fixtures) | ${m.definitions.count} / ${m.definitions.sixOrMoreParameters.models + m.definitions.sixOrMoreParameters.kernel + m.definitions.sixOrMoreParameters.fixtures} (${m.definitions.sixOrMoreParameters.models} / ${m.definitions.sixOrMoreParameters.kernel} / ${m.definitions.sixOrMoreParameters.fixtures}) |`,
+    `| Definitions taking two or more boolean parameters | ${m.definitions.twoBooleanParameters.length} (${m.definitions.twoBooleanParameters.join(', ') || 'none'}) |`,
     `| Free-text exclusion reasons in execution.json | ${m.exclusionReasons} |`,
   ].join('\n') + '\n';
 }
@@ -108,7 +152,7 @@ export function checkStyle({ directory = root, allowlist = JSON.parse(read(allow
   const failures = [];
   const listed = { lineLength: new Set(allowlist.lineLength ?? []), headerLength: new Set(allowlist.headerLength ?? []) };
   const files = quintFiles(directory);
-  for (const rule of Object.keys(listed)) for (const path of listed[rule]) if (!files.includes(path)) failures.push(`${allowlistPath}: ${rule} names a file that does not exist: ${path}`);
+  for (const rule of Object.keys(listed)) for (const path of listed[rule]) if (!files.includes(path)) failures.push(`${allowlistPath}: ${rule} names a file that is not a Quint source under formal/models: ${path}`);
   let checked = 0;
   for (const path of files) {
     const lines = read(path, directory).split('\n');
diff --git a/typescript/test/formal-style.test.ts b/typescript/test/formal-style.test.ts
index c5c28b17..672ac9f7 100644
--- a/typescript/test/formal-style.test.ts
+++ b/typescript/test/formal-style.test.ts
@@ -1,17 +1,27 @@
 import { mkdirSync, mkdtempSync, rmSync, writeFileSync } from "node:fs";
 import { tmpdir } from "node:os";
 import { join } from "node:path";
+import { fileURLToPath } from "node:url";
 import { afterEach, beforeEach, describe, expect, it } from "vitest";
 
-const { checkStyle, measure, renderReport, headerLines, caps } = await import(
+const { checkStyle, measure, renderReport, headerLines, definitions, caps } = await import(
   new URL("../../formal/tools/check-style.mjs", import.meta.url).href,
 ) as {
   checkStyle(options?: { directory?: string; allowlist?: { lineLength?: string[]; headerLength?: string[] } }): { files: number; lineLengthChecked: number; allowlisted: number };
-  measure(directory?: string): { files: number; linesOver: { total: number }; headers: { longest: number; overCap: number }; commentSentences: { over40: number }; definitions: { twoAdjacentBooleans: string[] }; exclusionReasons: number };
+  measure(directory?: string): {
+    files: number; linesOver: { total: number; fixtures: number }; headers: { longest: number; overCap: number };
+    commentSentences: { count: number; over40: number; longest: number }; guideSentences: { count: number; over40: number; longest: number };
+    definitions: { count: number; sixOrMoreParameters: { models: number; kernel: number; fixtures: number }; twoBooleanParameters: string[] }; exclusionReasons: number;
+  };
   renderReport(measurements: unknown): string;
   headerLines(lines: string[]): number;
+  definitions(text: string): Array<{ name: string; params: string[] }>;
   caps: { lineLength: number; headerLength: number };
 };
+const { validationPlan } = await import(new URL("../../formal/tools/validation.mjs", import.meta.url).href) as {
+  validationPlan(target: string, options: { directory: string }): Array<{ args?: string[] }>;
+};
+const root = fileURLToPath(new URL("../../", import.meta.url));
 
 describe("Quint style caps", () => {
   let directory: string;
@@ -25,48 +35,73 @@ describe("Quint style caps", () => {
     put("formal/models/clean.qnt", header(3));
     put("formal/models/kernel/tall.qnt", header(26));
     put("formal/models/fixtures/kernel/wide.qnt", `module w {\n${longLine}\n}\n`);
+    put("formal/models/fixtures/kernel/leading.qnt", [...Array.from({ length: 27 }, (_, i) => `// Leading line ${i + 1}.`), "module l {", "  pure val x = 1", "}", ""].join("\n"));
+    put("formal/models/defs.qnt", ["module d {", "  // ---- Banner line ----", "  // A sentence.", ...Array.from({ length: 5 }, () => `  // ${"word ".repeat(9).trim()}`), "  // ends.", "  pure def f(a: int, b: bool, c: int, d: bool) = a",
+      "  action g(x: bool, y: bool): bool = true", "  pure def h(a: int, b: int, c: int, d: int, e: int, f: int) = a", "  pure def k(step: (int, int) => int, v: bool) = v", "}", ""].join("\n"));
     put("formal/guides/GUIDE.md", "# Guide\n\nShort sentence. " + "word ".repeat(45) + "ends here.\n");
     put("formal/README.md", "# Formal\n\nOne sentence.\n");
     put("formal/catalogs/execution.json", JSON.stringify({ challenges: [{ reproducer: { exclusions: { a: "free text", b: { reason: "slug" } } } }] }));
-    put("formal/catalogs/style-allowlist.json", JSON.stringify({ lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: ["formal/models/kernel/tall.qnt"] }));
+    put("formal/catalogs/style-allowlist.json", JSON.stringify({ lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: ["formal/models/kernel/tall.qnt", "formal/models/fixtures/kernel/leading.qnt"] }));
   });
   afterEach(() => rmSync(directory, { recursive: true, force: true }));
 
   it("passes when every offender is allowlisted and counts what it checked", () => {
-    expect(checkStyle({ directory })).toEqual({ files: 3, lineLengthChecked: 2, allowlisted: 2 });
+    expect(checkStyle({ directory })).toEqual({ files: 5, lineLengthChecked: 4, allowlisted: 3 });
   });
 
   it("fails a long line and a tall header in files that are not allowlisted, naming the line", () => {
-    expect(() => checkStyle({ directory, allowlist: { lineLength: [], headerLength: ["formal/models/kernel/tall.qnt"] } }))
+    expect(() => checkStyle({ directory, allowlist: { lineLength: [], headerLength: ["formal/models/kernel/tall.qnt", "formal/models/fixtures/kernel/leading.qnt"] } }))
       .toThrow(/^formal\/models\/fixtures\/kernel\/wide.qnt:2: line over 120 characters$/m);
-    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: [] } }))
+    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: ["formal/models/fixtures/kernel/leading.qnt"] } }))
       .toThrow(/tall.qnt: module header has 26 comment lines \(cap 25\)/);
+    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: ["formal/models/kernel/tall.qnt"] } }))
+      .toThrow(/leading.qnt: module header has 27 comment lines/);
   });
 
-  it("fails a stale allowlist entry so the list only shrinks, and a missing file", () => {
-    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt", "formal/models/clean.qnt"], headerLength: ["formal/models/kernel/tall.qnt"] } }))
+  it("fails a stale entry for either rule, a file outside the scope, and reports both when a file offends the other rule only", () => {
+    const base = { lineLength: ["formal/models/fixtures/kernel/wide.qnt"], headerLength: ["formal/models/kernel/tall.qnt", "formal/models/fixtures/kernel/leading.qnt"] };
+    expect(() => checkStyle({ directory, allowlist: { ...base, lineLength: [...base.lineLength, "formal/models/clean.qnt"] } }))
       .toThrow(/clean.qnt has no line over 120; delete its lineLength entry/);
-    expect(() => checkStyle({ directory, allowlist: { lineLength: ["formal/models/fixtures/kernel/wide.qnt", "formal/models/missing.qnt"], headerLength: ["formal/models/kernel/tall.qnt"] } }))
-      .toThrow(/names a file that does not exist: formal\/models\/missing.qnt/);
+    expect(() => checkStyle({ directory, allowlist: { ...base, headerLength: [...base.headerLength, "formal/models/clean.qnt"] } }))
+      .toThrow(/clean.qnt has a header within 25 lines; delete its headerLength entry/);
+    expect(() => checkStyle({ directory, allowlist: { ...base, lineLength: [...base.lineLength, "typescript/test/fixtures/missing.qnt"] } }))
+      .toThrow(/names a file that is not a Quint source under formal\/models: typescript\/test\/fixtures\/missing.qnt/);
+    const swapped = () => checkStyle({ directory, allowlist: { lineLength: ["formal/models/kernel/tall.qnt", "formal/models/fixtures/kernel/leading.qnt"], headerLength: ["formal/models/fixtures/kernel/wide.qnt"] } });
+    expect(swapped).toThrow(/tall.qnt has no line over 120/);
+    expect(swapped).toThrow(/tall.qnt: module header has 26 comment lines/);
+    expect(swapped).toThrow(/wide.qnt:2: line over 120 characters/);
   });
 
-  it("measures headers from the module line to the first non-comment line", () => {
+  it("measures the header on both sides of the module line, stopping at the first import or definition", () => {
     expect(headerLines(["module m {", "  // a", "", "  // b", "  import x.* from \"./x\"", "  // not header", "}"])).toBe(2);
-    expect(headerLines(["// file comment", "module m {", "  pure val x = 1"])).toBe(0);
+    expect(headerLines(["// one", "// two", "module m {", "  // three", "  pure val x = 1"])).toBe(3);
+    expect(headerLines(["// file comment", "", "pure val before = 1", "// not adjacent", "module m {", "  pure val x = 1"])).toBe(1);
+    expect(headerLines(["pure val x = 1"])).toBe(0);
+  });
+
+  it("scans definitions to the matching parenthesis and counts boolean parameters anywhere", () => {
+    const found = definitions('pure def f(a: int, b: bool, c: int, d: bool) = a\naction g(x: bool, y: bool): bool = true\npure def k(step: (int, int) => int, v: bool) = v');
+    expect(found.map(d => [d.name, d.params.length])).toEqual([["f", 4], ["g", 2], ["k", 2]]);
+    expect(found[2]!.params[0]).toBe("step: (int, int) => int");
   });
 
   it("reports the measurements the readability plan tracks", () => {
     const m = measure(directory);
-    expect(m).toMatchObject({ files: 3, linesOver: { total: 1, fixtures: 1 }, headers: { longest: 26, overCap: 1 }, exclusionReasons: 1 });
-    expect(m.commentSentences.over40).toBe(0);
+    expect(m).toMatchObject({ files: 5, linesOver: { total: 1, fixtures: 1 }, headers: { longest: 27, overCap: 2 }, exclusionReasons: 1 });
+    expect(m.commentSentences).toMatchObject({ over40: 1 });
+    expect(m.commentSentences.longest).toBeLessThan(60);
+    expect(m.guideSentences).toMatchObject({ over40: 1 });
+    expect(m.definitions).toMatchObject({ count: 4, sixOrMoreParameters: { models: 1, kernel: 0, fixtures: 0 }, twoBooleanParameters: ["defs.qnt:f", "defs.qnt:g"] });
     const report = renderReport(m);
     expect(report).toContain(`| Lines over ${caps.lineLength} characters (models / kernel / fixtures) | 1 (0 / 0 / 1) |`);
     expect(report).toContain("| Free-text exclusion reasons in execution.json | 1 |");
+    expect(report).toContain("defs.qnt:f, defs.qnt:g");
   });
 
-  it("holds on the committed tree: every current offender is allowlisted and no allowlist entry is stale", () => {
+  it("holds on the committed tree and runs in the audit lane", () => {
     const result = checkStyle();
     expect(result.files).toBeGreaterThan(50);
-    expect(measure().headers.overCap).toBe(0);
+    expect(measure().headers.overCap).toBe(2);
+    expect(validationPlan("audit", { directory: root }).some(step => step.args?.[0] === "formal/tools/check-style.mjs")).toBe(true);
   });
 });