diff --git a/formal/catalogs/README.md b/formal/catalogs/README.md
index 14d37151..8c6d5127 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`; 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 7cb31144..b4a7585b 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": "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
new file mode 100644
index 00000000..99f953fe
--- /dev/null
+++ b/formal/catalogs/style-allowlist.json
@@ -0,0 +1,68 @@
+{
+  "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": [
+    "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 0ba0db8c..c8a4221a 100644
--- a/formal/guides/AUTHORING.md
+++ b/formal/guides/AUTHORING.md
@@ -78,7 +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.
+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 `.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 3ce7ca0b..fc8a6365 100644
--- a/formal/tools/README.md
+++ b/formal/tools/README.md
@@ -13,12 +13,16 @@ 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`).
diff --git a/formal/tools/check-style.mjs b/formal/tools/check-style.mjs
new file mode 100644
index 00000000..cb3e4aa6
--- /dev/null
+++ b/formal/tools/check-style.mjs
@@ -0,0 +1,175 @@
+// 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
+// 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 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';
+
+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 (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++;
+    else if (trimmed !== '') break;
+  }
+  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 };
+  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) {
+    const text = read(path, directory);
+    const lines = text.split('\n');
+    const over = lines.filter(line => line.length > caps.lineLength).length;
+    longLines += over;
+    areas[area(path)] += over;
+    const header = headerLines(lines);
+    headerTotal += header; headerMax = Math.max(headerMax, header); headersOver += header > caps.headerLength;
+    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 = [];
+  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;
+  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: distribution(commentWords),
+    guideSentences: distribution(guideWords),
+    definitions: { count: definitionCount, sixOrMoreParameters: wide, twoBooleanParameters: 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 / 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';
+}
+
+// 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 is not a Quint source under formal/models: ${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..672ac9f7
--- /dev/null
+++ b/typescript/test/formal-style.test.ts
@@ -0,0 +1,107 @@
+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, 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; 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;
+  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/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", "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: 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", "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: ["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 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: { ...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 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(["// 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: 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 and runs in the audit lane", () => {
+    const result = checkStyle();
+    expect(result.files).toBeGreaterThan(50);
+    expect(measure().headers.overCap).toBe(2);
+    expect(validationPlan("audit", { directory: root }).some(step => step.args?.[0] === "formal/tools/check-style.mjs")).toBe(true);
+  });
+});