Repository navigation
docs(rfc): propose model checking protocols with TLA+ - #827
Draft
behinddwalls wants to merge 1 commit into
Draft
behinddwalls wants to merge 1 commit into
behinddwalls wants to merge 1 commit into
Conversation
## Summary
### Why?
Nine of our last eleven serious bugs were protocol bugs between controllers or services: dead letters, lost acks, CAS races, dedup. Every one was found by a demo run, a hung test, or a reviewer, never by a test written to find it. More e2e coverage cannot fix that, because each run samples one ordering and each pinned ordering needs a hand-built lever.
### What?
- `doc/rfc/tla-plus.md`: proposal covering when a change needs a TLA+ spec, the `spec/{domain}/{protocol}/` layout, CI, staged ties to the Go code, a rollout with a stop criterion, and why e2e and integration tests cannot close the gap.
- `spec/submitqueue/landoutcome/`: a spec of a batch going from `landing` to terminal across orchestrator and Runway, plus a matrix of 24 DLQ and Runway design combinations with the expected verdict for each. It found #819 and #820, and showed that both obvious fixes are wrong.
- `tool/tlc/`: a Python runner and a `tlc_matrix_test` macro. The TLA+ tools JAR is pinned in `MODULE.bazel` and runs on a downloaded JDK (`--java_runtime_version=remotejdk_21`), so nobody installs Java or fetches a JAR, locally or in CI.
## Test Plan
✅ `bazel test //spec/submitqueue/landoutcome:matrix_test`: all 24 verdicts match, in about 6s; `--runs_per_test=10` stable
✅ a deliberately wrong expectation fails the test
✅ `make tidy`, `make gazelle`, and `make fmt` leave the tree unchanged; license linter; `//tool/docsite:site_test`
## Issue
Part of #819, #820
behinddwalls
force-pushed
the
tla-exploration
branch
from
October 8, 2026 16:42
13063d7 to
968bbf9
Compare
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Why?
Nine of our last eleven serious bugs were protocol bugs between controllers or services: dead letters, lost acks, CAS races, dedup. Every one was found by a demo run, a hung test, or a reviewer, never by a test written to find it. More e2e coverage cannot fix that, because each run samples one ordering and each pinned ordering needs a hand-built lever.
What?
doc/rfc/tla-plus.md: proposal covering when a change needs a TLA+ spec, thespec/{domain}/{protocol}/layout, CI, staged ties to the Go code, a rollout with a stop criterion, and why e2e and integration tests cannot close the gap.spec/submitqueue/landoutcome/: a spec of a batch going fromlandingto terminal across orchestrator and Runway, plus a matrix of 24 DLQ and Runway design combinations with the expected verdict for each. It found Land and landsignal DLQs fail alandingbatch that Runway goes on to merge #819 and Runway DLQ answers FAILED for a merge whose push already landed #820, and showed that both obvious fixes are wrong.tool/tlc/: a Python runner and atlc_matrix_testmacro. The TLA+ tools JAR is pinned inMODULE.bazeland runs on a downloaded JDK (--java_runtime_version=remotejdk_21), so nobody installs Java or fetches a JAR, locally or in CI.Test Plan
✅
bazel test //spec/submitqueue/landoutcome:matrix_test: all 24 verdicts match, in about 6s;--runs_per_test=10stable✅ a deliberately wrong expectation fails the test
✅
make tidy,make gazelle, andmake fmtleave the tree unchanged; license linter;//tool/docsite:site_testIssue
Part of #819, #820
🤖 Generated with Claude Code