[DO NOT MERGE] Formal verification reference: TLA+/Lean models, defect catalogue and fix plans

[joaodinissf]

Caution

Do not merge. This PR is a reference for the formal-verification campaign. Its fixes land as separate PRs.

Why the change

This keeps the formal models, the defect catalogue and the failing-first tests of the formal-verification campaign in one reviewable place, as the source for small, separate fix PRs.

Special things to note

• Not meant to be merged. Fixes land as their own PRs, in the order proposed in formal/BUGS.md §5. So far fix(release): compute the next version from tags reachable from the branch #1550 (PIPE-2), fix(xtext): match case-sensitive pattern lookups against the candidate name #1551 (TRIE-1) and fix(xtext.ui): iterate a snapshot of the matches when showing a running search #1552 (REF-2) are merged; fix(builder): abandon the load operation when a resource load times out #1553 (LDR-1) is open.
• 51 findings, 49 of them confirmed by a failing Java test or by at least 2 of 3 independent reviewers. The models are bounded checks and abstract proofs, not a proof that the Java code is correct.
• formal/check.sh does not yet fail when a theorem depends on a forbidden axiom (BAD:), so --update can accept one. No current proof is affected.

Change outline

+formal/
+├── parallel-loader/   tla/ lean/    # ParallelResourceLoader timeouts (LDR)
+├── find-refs/         tla/ lean/    # find-references result view (REF)
+├── binary-storage/    tla/ lean/    # binary model storage in the builder (STO)
+├── trie/              tla/ lean/    # qualified-name lookup ranges (TRIE)
+├── pipeline/          tla/ lean/    # release and snapshot workflows (PIPE)
+├── readonly/          comparator/ orphans/   # read-only checks (RO)
+├── BUGS.md            # defect catalogue, fix plans, fix-PR order
+├── REPORT.md          # campaign analysis
+└── check.sh           # runs the TLC and Lean checks
 com.avaloq.tools.ddk.xtext.test, com.avaloq.tools.ddk.xtext.ui.test
+  @Disabled failing-first tests for findings without a merged fix

Fix status:

PIPE-2  high    #1550  merged
TRIE-1  high    #1551  merged     test enabled on master
REF-2   low     #1552  merged     test enabled on master
LDR-1   medium  #1553  open       a timeout abandons the load operation
TRIE-2, PIPE-1, PIPE-3 (high) and 8 medium findings: no fix PR yet

🤖 Generated with Claude Code