docs(formal): explain the setup top to bottom on the landing README

[lan17]

Part of #220 (make formal/ readable for humans and agents).

Why

formal/README.md routed well and explained little. Its only top-down section ("How the specification connects to code") named no tool, artifact or lane, about 900 of its 1,850 prose words were toolchain pins and make-target semantics, and its 17-row profile table duplicated models/README.md. A newcomer could find the right guide but could not learn how the pieces fit without reading several of them.

What changes

• The setup, top to bottom. Six numbered stages (state the rule, check the models, generate, replay in every port, account for the evidence, gate a change). Each names its directory, its tool, what it produces and where to read more. A Mermaid data-flow diagram summarizes the same information; the text carries everything the diagram shows, so an agent reading the source loses nothing.
• Pipelines. The three workflows (CI, Formal smoke with the four differential shards, Full formal verification) as a second Mermaid diagram plus one paragraph each: trigger, what runs, what it proves, how long it takes (measured: docs-only PR lanes in minutes, differential shards up to ~30 min when a Quint input changed, the scheduled full run ~2.5 h).
• Reference. Every part of the system one hop away: guides by kind, generated views, every Quint model (helpers, verification, the 17 profiles, connection and wire models), every catalog and ledger, the replay modules and the main tools. The task table and directory table stay.
• Moved, not dropped. Toolchain, Docker, Java and environment-variable prose → new VALIDATION.md#prerequisites; the trace-replay commands → VALIDATION.md#reproducing-one-history; the local-clock insertion-instant note → the profile's line in models/README.md. The 17-row profile table is replaced by inline links plus pointers to models/README.md and PROFILES.md.
• ITF defined. The guides used "ITF" about forty times without expanding it. New glossary entry for the Informal Trace Format (the Apalache ADR-015 definition, the Quint CLI --out-itf reference, the trace shape and bigint encoding, where the histories here live, owner replay/itf.mjs), linked at the term's first use in the README and the behavior, conformance and porting guides.
• Repointed anchors. Eleven links in eight guides, go/README.md and docs/maintainers.md pointed at the removed README sections; they now point at #run-it, VALIDATION.md#prerequisites or models/README.md. The link checker validates files, not anchors, so these would have gone dead silently.

Measurements

	before	after
Prose words (outside code and diagram fences)	1,848	2,106
Lines	254	331
Distinct link targets	55	115 (none dropped)
Diagrams	0	2

The page grew by about a seventh while taking on the explanation it lacked and the reference list it was asked to keep.

Verification

• make audit green after check-source-audit.mjs --refresh on the eleven edited audited pages and check-go-parity.mjs --refresh-inputs.
• pnpm docs:check green (sources, 32 formal pages' relative links).
• vitest formal-source-audit and formal-style: 30 passed.
• Every #anchor in the new README resolves to a heading (script-checked); repo-wide grep finds no reference to a removed anchor.
• Docs only: no Quint, TypeScript, Go, Rust or Python source changes.

Follow-up worth considering

scripts/check-docs.mjs checkFormalLinks checks that a linked file exists but not that its #anchor matches a heading; this PR would have broken eleven anchors without it being noticed. A small extension would close that.

🤖 Generated with Claude Code

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 93.73%. Comparing base (5030320) to head (5149ad3).

Additional details and impacted files

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

Flag	Coverage Δ
go	91.12% <ø> (ø)
python	92.08% <ø> (ø)
rust	94.29% <ø> (ø)
typescript	96.56% <ø> (ø)

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

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

🚀 New features to boost your workflow:

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