adapter: Add TLA+ formal verification of timestamp selection

[antiguru]

Summary

• Adds a TLA+ specification modeling the constraint solver in determine_timestamp_via_constraints over a bounded timestamp domain (0..4)
• Covers all three isolation levels (Serializable, StrictSerializable, StrongSessionSerializable) and all QueryWhen variants
• TLC exhaustively verifies 750k input combinations checking: lower/upper bound respect, real-time ordering, completeness, soundness, and preference correctness
• Packaged as an mzcompose test with a Docker container running the TLC model checker

Test plan

• bin/mzcompose --find tla run timestamp-selection passes locally (750k states, 6s, all 7 properties verified)
• Integrate in CI pipeline

TODO: Integrate the check in ci/test/pipeline.template.yml

🤖 Generated with Claude Code

[github-actions]

Thanks for opening this PR! Here are a few tips to help make the review process smooth for everyone.

PR title guidelines

• Use imperative mood: "Fix X" not "Fixed X" or "Fixes X"
• Be specific: "Fix panic in catalog sync when controller restarts" not "Fix bug" or "Update catalog code"
• Prefix with area if helpful: compute: , storage: , adapter: , sql:

Pre-merge checklist

• The PR title is descriptive and will make sense in the git log.
• This PR has adequate test coverage / QA involvement has been duly considered. (trigger-ci for additional test/nightly runs)
• If this PR includes major user-facing behavior changes, I have pinged the relevant PM to schedule a changelog post.
• This PR has an associated up-to-date design doc, is a design doc (template), or is sufficiently small to not require a design.
• If this PR evolves an existing $T ⇔ Proto$T mapping (possibly in a backwards-incompatible way), then it is tagged with a T-proto label.
• If this PR will require changes to cloud orchestration or tests, there is a companion cloud PR to account for those changes that is tagged with the release-blocker label (example).