docs(formal): describe all four ports in the formal guides

[lan17]

Why

The reviewed formal guides predate the Python port (#200).
formal/catalogs/profiles.json declares all 17 profiles for typescript, go,
rust and python, make formal runs formal-python, and the full formal
workflow gates on a python-parity lane. The guides still described two or three
ports. Step 4 of AUTHORING.md's "Codifying the next behavior", the workflow
agents follow for new behavior, said to replay "in TypeScript, Go and Rust".

What

Every statement about which ports replay the corpus, carry a replay mechanism or
must be exercised now names TypeScript, Go, Rust and Python. Each was checked
against formal/tools/validation.mjs, formal/tools/conformance.mjs,
formal/tools/explore.mjs, .github/workflows/formal-full.yaml and
python/tests/ before it changed.

• formal/README.md: four implementations in the task table and the
  walkthrough pointer; Python 3.11+ and python/.venv setup in the
  prerequisites; make formal-python in the lane list; seven parallel hosted
  lanes (four parity, three mutation) instead of six.
• AUTHORING.md: Python in the opening contract sentence, the walkthrough
  summary and step 4. The fault-detection paragraph now says Python has no
  native mutation campaign.
• WALKTHROUGH.md: Python driver and replay-transport rows, and the Python
  command that replays the example history.
• PORTING.md: the Python driver link; Go, Rust and Python share the
  JSON-lines coordinator transport; each port's no-settle control (Rust and
  Python already have one); the Python prepare, adapter and check commands,
  default source inventory and witness-evidence inputs.
• VALIDATION.md: Python in full acceptance, the lane list, the 90-day
  formal-summary artifact and exploration ordering. make mutations covers
  TypeScript, Go and Rust only.
• BEHAVIOR, CONFORMANCE, CONTRACTS, FEATURE-COVERAGE, SEMANTIC-COVERAGE, SPEC,
  TEST-AUDIT, TEST-MAP: replay statements that said "both ports" or
  "TypeScript and Go" now say every port or list all four.
• Pins: source-audit.json guide hashes and heading line numbers, and
  go-parity.json sourceAuditSha256. Only hashes and line numbers changed.

This PR changes no Quint models, profiles, replay code or behavior.

Left scoped to fewer ports on purpose

• Native mutant mappings (nativeMutants, the mutations.json sections),
  generated-cohort fault detection and the mutation boundary gate cover
  TypeScript and Go only. Rust keeps its note about its separate catalog.
• FEATURE-COVERAGE.md's native checks "in both languages": the native cases in
  feature-coverage.json name only TypeScript and Go tests.
• The causal publication monitor exists only in the TypeScript, Go and Rust
  drivers. SPEC.md and SEMANTIC-COVERAGE.md now name those three instead of
  "both drivers".
• VALIDATION.md's dated exploration records ("passed both ports") describe
  two-port runs and stay as history.
• Go-specific statements in GO-PARITY.md and PROTOCOL.md.

Design-record pointers skipped

#225 adds design/README.md but has not merged; design/README.md is not on
origin/main. This PR therefore leaves out the design-record row in
formal/README.md's task table and the opening sentence in AUTHORING.md's
"Codifying the next behavior". Both can follow once #225 lands.

Gaps noticed, not changed

• Python has no native mutation campaign and no causal publication monitor.
  PORTING.md's "New-port acceptance" asks for representative semantic mutations.
• BEHAVIOR.md "Port workflow and limits", step 4 lists 9 of the 17 profiles.
• formal/tools/explore.mjs still logs "both native witness leaves record the
  shortfall" when the tolerated witness step fails.

Verified

• make audit and node scripts/check-docs.mjs pass on Node 24.20.0, as does
  typescript/test/formal-source-audit.test.ts.
• The new walkthrough Python command: exported
  heldPolicyDoesNotSpendSourceBudgetTest with Quint 0.32.0, then
  node formal/tools/run-python-replay.mjs --profile=source-budgets --trace=…
  passed (1 case, 8 steps).
• Docs and pins only, so this needs no full formal run.

[codecov-commenter]

Codecov Report

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

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #226      +/-   ##
==========================================
- Coverage   93.73%   93.73%   -0.01%     
==========================================
  Files          78       78              
  Lines       11357    11357              
  Branches      656      656              
==========================================
- Hits        10646    10645       -1     
- Misses        641      642       +1     
  Partials       70       70              

Flag	Coverage Δ
go	91.12% <ø> (-0.06%)	⬇️
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.