Verification — How a Formatter Proves It Did Not Break Your Code
A formatter is a program that rewrites every line of your source. The question "how do you know it didn't change anything?" has a real answer, a literature, and — across the systems surveyed here — an enormous variance in how seriously it is taken. This page collects the practice, ranks it, and turns it into the contract the D proposal builds first, before any layout code.
Last reviewed: August 15, 2026
The three properties
From the concepts vocabulary and de Jonge & Visser's equations, specialized to a formatter:
| Property | Statement | What it catches |
|---|---|---|
| Semantic preservation | PARSE(FORMAT(s)) ≡ PARSE(s) | the formatter changed the program |
| Idempotence | FORMAT(FORMAT(s)) = FORMAT(s) | the formatter disagrees with itself |
| Totality | FORMAT(s) terminates without crashing, for all valid s | the formatter panics or hangs |
De Jonge & Visser's Correctness criterion, PARSE(CONSTRTEXT(TRANSF(PARSE(s)))) = TRANSF(PARSE(s)), is the first row with TRANSF = id. Their Preservation criterion, CONSTRTEXT(PARSE(s)) = s, is too strong for a formatter as a whole — a formatter is supposed to change layout — but it is exactly right, unweakened, for the regions a formatter declines to touch: verbatim regions, // fmt off ranges, and everything outside a range-format request.
The ladder, as practised
Ranked by strength, with who does what:
| Tier | Check | Cost | Practised by |
|---|---|---|---|
| 0 | Nothing — a test suite and hope | — | dfmt ("Make backups of your files"), zig fmt |
| 1 | Golden-file corpus | cheap | gofmt (testdata/*.golden), everyone |
| 2 | Idempotence in CI — format twice, diff | cheap | ruff, dart_style |
| 3 | Token equality modulo whitespace — lex both, compare non-trivia tokens | cheap, needs a lexer | — |
| 4 | AST equality on reparse, in CI | moderate | black, prettier (--debug-check) |
| 5 | AST equality at runtime, every file | expensive | ocamlformat |
| 6 | + trivia-specific checks (comments survived, docstrings did not move) | expensive | ocamlformat alone |
| 7 | Convergence enforced — iterate to a fixed point or fail | expensive | ocamlformat alone |
Nobody is above tier 7, and only one system is above tier 4. For a class of tool that rewrites every line of every file, that is a striking distribution.
The reference implementation: ocamlformat
OCamlFormat's print_check loop is the only runtime verifier in the survey, and its design is worth copying whole. Per file, per run:
- Reparse the output.
- AST equality —
Normalize_std_ast.equal std_fg conf std_t.ast std_t_new.ast; on failure, dump both normalized ASTs to.unequal-astfiles. - A separate docstring check — re-compare with
~ignore_doc_comments:true; if that passes while step 2 failed,Normalize_std_ast.moved_docstringsnames the docstrings that moved. - Comment check —
check_comments ~old ~new_, pluscheck_all_locations. - Iterate — recurse until output stabilizes, or fail with
Unstable {iteration; prev; next; input_name}atmax-iters(default 10).
Three design choices generalize:
- Normalize before comparing. A raw AST comparison fails on irrelevant differences (positions). The normalization is the specification of what the formatter is allowed to change.
- Separate the trivia check from the code check. "The code is identical but a docstring moved" is a different bug from "the code changed", with a different severity and a different fix. Collapsing them into one boolean loses the information that matters.
- Failure produces artifacts, not just an exit code.
.unequal-astdumps exist because this class of bug is rare and impossible to debug from a diff of formatted output.
The cheap alternative: ruff's ecosystem harness
ruff gets most of tiers 2–4 for a fraction of the runtime cost by moving the checks from the tool into CI, over real projects:
"The stability checks catch for three common problems: The second formatting pass looks different than the first (formatter instability or lack of idempotency), printing invalid syntax (e.g. missing parentheses around multiline expressions) and panics (mostly in debug assertions)." —
crates/ruff_python_formatter/CONTRIBUTING.md
That is idempotence + a weak form of semantic preservation + totality, on an ecosystem corpus, gating every change. Paired with the similarity index (see below) it is the best cost/assurance ratio in the survey.
The compatibility metric
For a formatter replacing an incumbent, there is a fourth property nobody else measures: how much does the output differ from the tool being replaced?
"It will print the similarity index, the percentage of lines that remains unchanged between Black's formatting and our formatting. You could compute it as the number of neutral lines in a diff divided by the neutral plus the removed lines. … You should ensure that your changes don't decrease the similarity index." —
CONTRIBUTING.md
A published definition, a single number, and a CI gate. For a D formatter succeeding dfmt this is directly applicable — and it remains useful even where the new formatter deliberately diverges, because then the index measures the size of the intended divergence rather than an accident.
What each surveyed system actually does
| System | Semantic preservation | Idempotence | Totality | Notes |
|---|---|---|---|---|
| ocamlformat | runtime AST equality | enforced, ≤ max-iters | errors as bug reports | + docstring-movement and comment checks |
| ruff | CI: output must reparse | CI, ecosystem corpus | CI: no panics | + similarity index gate |
| black | AST-equivalence tests | stability tests | fuzzing | comment loss is an admitted historical bug class |
| prettier | --debug-check (opt-in) | test suite | test suite | "exact same behavior" stated as requirement #1 |
| dart_style | — | format-twice test | — | |
| gofmt | — | golden corpus | golden corpus | |
| rustfmt | verbatim fallback preserves unformattable regions | — | — | --error-on-unformatted surfaces silent fallback |
| clang-format | — | — | — | very large regression suite; two silent search caps |
| dfmt | none | none | none | "Make backups of your files or use source control" |
| zig fmt | — | test suite | — | |
| topiary | refuses ERROR trees | idempotence in its own tests | — | @leaf gives byte-exact regions |
The contract for a D formatter
The proposal makes this M1 — before any layout code — because a verifier built after a printer is a verifier written to agree with the printer's existing bugs.
Tier 3 is the sweet spot for D, and it is unusually cheap here. If the formatter is built on a token spine (dfmt's architecture, and the proposal's Q-c), then the verifier already has a lexer, and token-equality-modulo-whitespace is a few dozen lines. It catches every class of error a formatter realistically produces — dropped tokens, mangled literals, lost comments — without a reparse.
The recommended stack, in build order:
- Round-trip the spine — reconstruct the input byte-for-byte from the token+trivia stream before any formatting exists. If this fails, nothing downstream can be trusted.
- Token equality modulo whitespace on every format, in
--checkand in tests. - A separate DDoc check. D has exactly OCaml's hazard: ddoc comments are semantically attached,
dmd-lspkeeps them alive deliberately, and a formatter that reattaches one has silently changed the generated documentation. It deserves its own check and its own error message, following ocamlformat'smoved_docstrings. - Idempotence, iterated to a fixed point with a bounded count; non-convergence is a reportable bug, not a curiosity.
- Ecosystem corpus in CI — Phobos, druntime,
sparkles— with ruff's three stability checks and the similarity index against dfmt, gated so it cannot decrease unintentionally. - Verbatim-region preservation, checked: for every
// dfmt offrange,asmblock,q{}token string and unformattable construct, assertFORMAT(s)reproduces those bytes exactly — de Jonge & Visser's Preservation criterion, applied where it actually holds.
Tiers 5–7 (runtime AST equality on every file) are worth revisiting only if the token check proves insufficient in practice; they cost a reparse per file and D's compile-time budget is already the binding constraint on the LSP path.
Sources
ocaml-ppx/ocamlformat@20c45431:lib/Translation_unit.ml,lib/Conf.mlastral-sh/ruff@3b067a16:crates/ruff_python_formatter/CONTRIBUTING.mdpsf/black@74371e20:docs/the_black_code_style/index.mddlang-community/dfmt@c65d1c8a:README.md- de Jonge & Visser 2011, §2 — the Correctness and Preservation criteria and the lens laws
Related deep-dives in this tree:Layout preservation · Concepts · ocamlformat · The Rust reimplementation wave · dfmt · Comparison · The proposal