consensus: add Lean proofs for Mysticeti v3 - #27687
Open
mwtian wants to merge 42 commits into
Open
Conversation
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 13, 2026 17:37 — with 
GitHub Actions
Active
GitHub Actions
Active
|
The latest updates on your projects. Learn more about Vercel for GitHub.
2 Skipped Deployments
|
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 14, 2026 04:03 — with
GitHub Actions
Active
GitHub Actions
Active
mwtian
force-pushed
the
tmw/mysticeti-v3-lean-main
branch
from
August 14, 2026 04:12
478a26c to
8b25f08
Compare
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 14, 2026 04:12 — with
GitHub Actions
Active
GitHub Actions
Active
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 14, 2026 05:30 — with
GitHub Actions
Active
GitHub Actions
Active
mwtian
force-pushed
the
tmw/mysticeti-v3-lean-main
branch
from
August 14, 2026 06:05
d11c5a2 to
f4ef67d
Compare
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 14, 2026 06:05 — with
GitHub Actions
Active
GitHub Actions
Active
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 14, 2026 14:25 — with
GitHub Actions
Active
GitHub Actions
Active
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 14, 2026 19:56 — with
GitHub Actions
Active
GitHub Actions
Active
mwtian
force-pushed
the
tmw/mysticeti-v3-lean-main
branch
from
August 15, 2026 04:40
7097b7d to
876dfab
Compare
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 15, 2026 04:40 — with
GitHub Actions
Active
GitHub Actions
Active
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 19, 2026 20:44 — with
GitHub Actions
Active
GitHub Actions
Active
The v3 schedule is adaptive. `LeaderScheduleV3` recomputes the allowed-leader vector from committed scores, so leader identity flows upward from the decisions below, while a decision flows downward from its anchor. Composed without a restriction, the verdict of a slot could depend on the leader of its own anchor, whose identity depends on that verdict. Two schedules could then each justify themselves. Rust already prevents this. `min_next_leader_round` is one round above the leader round of the last commit in the pending window. `FlexCommitter::maybe_refresh_pending_commit_state` asserts that the value is identical at one commit index, that it moves strictly forward with the index, and that a schedule change drops every pending round below the new gate. Model that gate. `V3ScheduleGateSequence.governing_commits_are_below_round` proves the stratification on the modeled state: every commit that feeds the schedule governing a round sits at a leader round below it. `adaptive_run_unique` then proves that at most one run of decisions is consistent with the rule, and `consistent_runs_are_equal` lifts that to every reading of the run. The common commit chain of `ASM-SAFE-COMMIT-CHAIN` therefore follows for the adaptive schedule rather than being assumed. What remains for that assumption is the refinement obligation that each correct host's behavior is a consistent run of one common rule.
`consistent_run_readings_agree` was a schema over an arbitrary reading of a run. Nothing instantiated it, so no theorem mentioned commits. Add the instantiation. `committedPrefix` is the ordered committed leaders of a run through a round bound, and `committed_prefix_agrees` proves that two consistent runs produce the same one. `v3_committed_candidates_agree` fixes the verdict to the exact commit candidate that a FlexCommitter round scan returns, so the statement is about commits rather than about an abstract reading. `v3_committed_leaders_agree` gives the leader-level form. The argument is induction on the round. Agreement below a round gives one schedule at that round, and one schedule gives one verdict. Prefix agreement is the conclusion at each step, not a hypothesis. Assuming it would assume `ASM-SAFE-COMMIT-CHAIN` itself. `adaptive_run_unique` uses no axiom.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 19, 2026 22:43 — with
GitHub Actions
Active
GitHub Actions
Active
Two gaps remained after the uniqueness proof. `ValidatorV3AdaptiveScheduleExistence` closes the first. `adaptive_run_exists_unique` proves that exactly one run agrees with the adaptive rule. The construction is strong recursion on the round. Values above the current round come from a fixed default, and the gate rules prove that the schedule never reads it, so the theorem needs no `Inhabited` instance. `ValidatorV3FlexScheduleRun` closes part of the second. `V3FlexScheduleHost.consistentRun` derives `ConsistentRun` for one modeled host from five local facts: the initial schedule, the no-commit step, the `add_commit` step, the selected order at the governing gate, and each post-scan slot. The proof reconstructs the modeled `LeaderScheduleV3` state from the host's own earlier verdicts. It does not assume `ConsistentRun`, and it does not compare two hosts. The cross-host step stays open. Uniqueness holds for two runs of one rule, so agreement still needs every correct host to use the same commit material, governing gate, and final slot function. Local DAG and GC views differ, so that step needs the protocol evidence and exact installation proofs. Record the revalidation trigger that this work created. The fixpoint rests on three assertions in `FlexCommitter::maybe_refresh_pending_commit_state`. Removing one removes the stratification, and no Lean build failure reports it.
`V3ScheduleGateSequence` took the governing commit index as a field, so two hosts could in principle govern one round with different indexes. They cannot. The gate moves strictly forward, so the largest index whose gate does not exceed a round is unique. Derive it. `derivedGoverningIndex` is `Nat.findGreatest` over the gate condition, `derived_gate_not_above` discharges the gate rule for every round at or above the first gate, and `derived_governing_is_greatest` shows no later index governs. `index_le_gate` supplies the search bound from the strictly increasing gate. `derived_governing_index_agrees` then removes one degree of freedom from the cross-host step: two hosts with the same schedule states govern each round with the same commit index, by construction rather than by assumption.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 19, 2026 23:56 — with
GitHub Actions
Active
GitHub Actions
Active
…l gives The cross-host step for `ASM-SAFE-COMMIT-CHAIN` cannot be full verdict equality. The Flex round scan stops at the first undecided selected slot, so a host with less evidence returns no candidate where a better informed host returns one. Their verdicts differ at that moment. A theorem that claimed otherwise would be false of a real execution. State agreement where both hosts have decided instead. `round_candidates_agree` gives one round, and `committed_candidates_agree_across_hosts` gives the installed sequence. The extra condition is that neither host is ahead of the other in deciding the round. A lagging host fails that condition until it decides, which is the correct behavior. The proof reuses the per-slot result. `final_reference_slot_decision_agrees` already concludes only when both sides are final, so the partiality was handled correctly in the slot layer. This lifts it to the round verdict and the run. The open condition is now `CrossViewExactSlotAgreement` for each selected slot. That is the named cross-view safety goal of `ReferenceFlexCommitter`, not a new assumption.
Safety has two parts, and the specification proves both. They sat in separate modules, and the aggregate `mysticeti_v3_safety` theorem covers only the first, so a reader could not see the second. Part one is per-slot exclusion. One selected leader slot cannot hold a commit result and a skip result at the same time, and one transaction cannot be accepted and rejected. Part two is same-index commit agreement. Two correct, available validators that have installed a commit at one index have installed the same commit. `ExactCommitPrefixSafety.exactInstalledHeadsAtSameIndexAgree` already proved it. The commit head carries the index, the commit identifier, and the leader round, so equality of heads is equality of the digest, and agreement at every index gives prefix agreement entry by entry. `MysticetiSafetyCapstone` names the two parts together and re-exports the second as `correct_validators_agree_on_commit_at_index`. Its docstring lists what part two assumes: authenticated Flex votes, which carry the quorum-evidence adapter, and install provenance, whose fields are one-host storage and hash-chain rules. No provenance field mentions two validators, and no field states agreement.
A change to `consensus/core` cannot break a Lean target, and the specification workflow does not run for such a change. The only link is the prose revalidation-trigger lines in the evidence ledger. Design a workflow job that reports which proof obligations a product change puts at risk. The job reads the diff, walks each hunk to its enclosing Rust item, and looks the item up in a checked-in map. It compiles nothing. Measurements over the last 200 commits of this branch: nine touch `consensus/core/src`, and one touches a proof-critical file. The job is therefore quiet rather than noisy, so each map entry must carry the consequence in prose and not only an identifier. Staleness is the failure that matters. A rename makes the map stop matching, and silence reads as no risk. The job must check that every mapped item still exists, and that check fails the build. Nothing is implemented.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 20, 2026 00:43 — with
GitHub Actions
Active
GitHub Actions
Active
`ExactCommitInstallProvenance.correct_validators_agree_on_commit_at_index` already proves the safety statement. Two correct, available validators that installed a commit at one index installed the same commit. Its inputs hold no cross-host equality: every field of `AuthenticatedFlexVoteSourceMap` and of `ExactCommitInstallProvenance` is a one-host rule. `ValidatorV3FlexScheduleRun` and `ValidatorV3FlexCrossHostAgreement` built a second route to the same conclusion through a common per-host model. That route needed cross-host agreement of the commit material and the post-scan slots, which the first route does not need. It added no safety result, and nothing outside those two files used any of it. Remove both files, 360 lines. The fixpoint work stays. It justifies the head-indexed signatures that the first route uses, such as `firstPendingRoundForHead`: the schedule recursion is stratified by the Rust gate, so exactly one run of decisions is consistent with the rule and the schedule is a function of the commit prefix.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 20, 2026 00:58 — with
GitHub Actions
Active
GitHub Actions
Active
Add a section to the proof scope that names the boundary, so a later reader does not plan work that cannot finish. The specification is a conditional model. A theorem applies to the product only when each source-map field is true of the running code. Proving that the Rust equals the Lean model is not achievable from the source alone. It needs extraction, code generation, or translation validation, and none of those exists here. The comparable `lean-dag` formalization does not attempt the step either; it names no Rust. List what is achievable instead: construct a source-map field from a model of one Rust function, keep the ledger statuses honest, add conformance tests, and report the obligations that a source change puts at risk. Give the worked example. `ASM-SAFE-EVIDENCE-REFINEMENT` needs the deciding anchor of an indirect result. Rust stores `Decision::Indirect`, one value of a three-value enumeration. It records that the indirect rule decided the slot, not which anchor decided it, and `FlexCommitter::try_indirect_decide` only logs the anchor reference. A restart or a leader-schedule reset rebuilds the pending state without that provenance, so the field cannot be filled from the current code.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 20, 2026 01:13 — with
GitHub Actions
Active
GitHub Actions
Active
An earlier commit recorded that a restart or a leader-schedule reset rebuilds the pending state and loses the provenance of an indirect decision. That is wrong, and `ASM-SAFE-EVIDENCE-REFINEMENT` carried the same mistaken premise. No decision is durable. `PendingCommitState` is in-memory, starts from its default value, and never reaches the store. `WriteBatch` carries accepted blocks, commits, commit info, and finalized commits with their rejected transaction indices. It carries no slot status and no decision origin. A restart recomputes every verdict from recovered blocks and commits, and `maybe_refresh_pending_commit_state` discards the pending rounds on a schedule change. No stale indirect result survives either event, so there is nothing to misclassify across them. The anchor search also starts at `min_next_leader_round` and reads pending rounds only, so a committed leader is never an anchor. The open part is narrower than recorded: within one pending-state lifetime, `Decision::Indirect` records that the indirect rule decided a slot, and `try_indirect_decide` only logs the deciding anchor. Replace the worked example in the proof scope with one that holds. Safety has 22 hypothesis fields across two structures and no module constructs either, and `ASM-SAFE-PARAMETERS` is a field the code is known to break. Add the instruction to check the store before recording a durability hazard. Record that Rust has two commit tables where the model has one durable notion. Both key on the same index and digest, so the single notion is adequate for commit agreement. Transaction outcomes are separate.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 20, 2026 01:25 — with
GitHub Actions
Active
GitHub Actions
Active
Split compound rows so each row holds one idea, and point every row at the exact goal-theorem input field it supplies. Rows that state what a proof derives lose that text; rows that supply no field are deleted. - `ASM-SAFE-COMMIT-CHAIN` becomes `ASM-SAFE-DIGEST-IDENTITY`, `ASM-SAFE-COMMIT-STORE`, and `ASM-SAFE-INSTALL-PROVENANCE`. The chain rule is no longer assumed: `ValidatorCommitHead` now carries `previousId`, the same back-link as `CommitV1.previous_digest`, `DigestLinkedCommits` defines the chain check, and `digest_chain_entry_matches_installed_prefix` derives the chain-to-prefix rule from the digest row and the gap-free store. - `ASM-SAFE-FIRST-TRIGGER` now states the actual finalizer queue: compare the newest commit's leader round with the earliest one's, then run the indirect rule on the earliest commit and pop it. - `ASM-SAFE-NON-EQUIVOCATION` keeps the signing rule and covers its transaction-vote field. The counting rule moves to `ASM-SAFE-VOTE-SET-OVERLAP`, whose leader half is already derived by `twoViewEvidence`; the certificate and transaction halves are not. - `ASM-LIVE-LEADER` splits into `ASM-LIVE-LEADER-STAKE` and `ASM-LIVE-LEADER-SCHEDULE`, and the schedule row now names only fields that exist. `ASM-SAFE-EVIDENCE-REFINEMENT` moves its cached-anchor half to `ASM-SAFE-INDIRECT-ORIGIN`. `ASM-SAFE-GC` moves its frontier half to `ASM-LIVE-GC-FRONTIER`, which points at the CL `retention` binder. `ASM-LIVE-FINITE-REFERENCE-SPACE` keeps the finite encoding and moves its capsule half to `ASM-LIVE-CAPSULE-PROJECTION`. - `ASM-LIVE-COMMIT-SYNC` folds into `ASM-LIVE-TASK-FAIRNESS`; only its non-starvation content was an assumption. `ASM-LIVE-DURABILITY` keeps the stage timing bounds; the durable-before-exposure facts become `REF-DURABLE-PROPOSAL` and `REF-DURABLE-COMMIT-OUTPUT`, and restart is described in the proof scope. Complete the source map so every rule-bearing input field of a goal theorem has an owner row, and add a structural-fields note for the data fields that define the model itself. The time-zero boundary fields `initial` and `genesisParents` get the new row `ASM-LIVE-COMMON-GENESIS`, and `authorityCountAtLeastTwo` joins `ASM-SAFE-PARAMETERS`. Delete the dead `localGcCutoffCausal`, `exactAnchorCausalData`, and `flexCausalView` inputs, the unconsumed Flex-scan cutoff structure, and the replay, durable-work, remote-commit-traffic, and action-scoped-leader-parent modules that no goal theorem consumes. The ledger check now accepts five type kinds and covers 38 rows with 56 Rust mappings.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 20, 2026 07:15 — with
GitHub Actions
Active
GitHub Actions
Active
Verify the assumption rows against the current Rust and against the in-progress branch `tmw/mysticeti-v3-transaction-voting`, which the product intends to merge. A new ledger convention marks rows whose evidence comes from that branch; they revalidate on merge. Restate `ASM-SAFE-FIRST-TRIGGER` with the v3 finalizer algorithm: each new commit reruns direct finalization for all pending commits; the first local descendant on each authority chain can give an implicit accept vote through the round after the commit leader; the vote tracker supplies explicit rejects; indirect finalization uses only committed descendants with certification stake; the shared depth-two trigger rejects the remainder, so depth two is the latest release point. `ASM-LIVE-FINALIZER-TRIGGER` moves from a known mismatch to an open proof obligation: the trigger path now exists, and what remains is to derive the arrival of a deep enough commit from commit liveness. Correct rows against the branch code: the signed cutoff is at least the block-cleanup and vote-cleanup rounds and vote-target truncation can raise it; the proposer computes it live in `try_new_block`; the slot decider, the FlexCommitter, and the v3 finalizer share one indirect depth. Refresh the non-finalizer rows against current code: the core handler gate, the own-round fetch trigger, the proposal flush, the direct and indirect decision rules, the scan bounds, the commit timestamp rule, and the schedule reader behavior. Update the Lean model to the branch vote semantics. A vote's target must only be below its voting round, because first-descendant votes span mixed rounds. A block that does not accept supplies no stake, so the reject-side lemmas are deleted; explicit rejects and the depth-two trigger carry rejection. `cutoffCoversGc` replaces the cutoff-equality field, and `accepts_only_above_gc` is reproved from the inequality.
mwtian
deployed
to
sui-typescript-aws-kms-test-env
August 22, 2026 17:16 — with
GitHub Actions
Active
GitHub Actions
Active
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.
Description
This is an attempt to bridge Mysticeti v3 implementation in Rust to a specification in Lean with provable safety and liveness under partial synchrony.
The theoretical specifications of Mysticeti have been proven manually (https://arxiv.org/abs/2310.14821), and with AI assistance (https://github.com/gdanezis/lean-dag). But there are some gaps between the proven specs and the actual implementation. Proving safety and liveness closely based on the actual Rust implementation is also almost impossible, even if we are allowed to acknowledge implementation gaps, because the proof will likely be bogged down in deriving guarantees from detailed behaviors.
Here, the explicit assumptions that went into the Lean spec and proofs are more detailed and realistic than usual proofs, but still not exactly the implementations. For example:
The goal for this specification is to provide a foundation to help us reason about the correctness of future protocol changes in future.
Test plan
CI