Repository navigation
test: add formal verification of the leaderless signaling protocol - #4
Merged
Merged
Conversation
Signed-off-by: Hang Yin <h4x3rotab@gmail.com> # Conflicts: # README.md
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
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
Formal-verification-only follow-up to merged implementation PR #3. This PR now targets
main; its diff contains only the verification package, CI, documentation links, and ignore rules.protocol/TLA+ models, negative controls, reachability witnesses, and pinned TLC runner.No runtime code or deployment configuration changes relative to implementation PR #3. This branch is synchronized with #3's native single-apply deployment and inline-env coordinator module; the formal package itself and signaling runtime hashes remain unchanged from the originally checked combined source.
Evidence and claim boundaries
The package previously passed 35/35 TLC expectations and 104 Lean kernel-checked declarations, with no placeholders or custom axioms. Its CI jobs also passed on the original combined PR; this split reruns them independently.
The unbounded theorem proves signaling-state convergence, mutual credential knowledge, and stable-epoch candidate dissemination. Premises include authenticated honest fixed membership, fresh identifiers, unbounded counters, finite external resets, fair processing/publication, and recurring timely common-broker lease windows. Protocol-induced renegotiation termination is derived, not assumed.
It does not prove Go implementation refinement, attestation/crypto correctness, finite timeout resets, NAT mapping usability, bounded latency, or ICE connection success. The finite composed-recovery TLA+ checks and the unbounded Lean specification are separate evidence; no equivalence is claimed.
See
protocol/README.mdandprotocol/proof/README.mdfor exact model bounds, assumptions, and proof scope.