Proof is powerful
when its scope is exact
Replacing trust with proof only counts when the proof's scope is exact. Astrea combines empirical tests with machine-checked mathematics: tests exercise executable behavior under concrete conditions, and Lean checks that a precise consensus theorem follows from its stated model and assumptions. Each answers a different question, and this page shows how to read both.
Different evidence catches different failures
A test runs a real example and checks the observed result. It can expose an implementation bug, a bad boundary case, or a surprising interaction. A mathematical proof starts from stated assumptions and covers every case represented by its model. Machine checking then verifies that no logical step has been skipped.
Tests establish how selected executions behaved. A theorem establishes that a property follows for every state admitted by its model. A green test run cannot establish the second claim, and a theorem about a model cannot replace testing the software and environment around it.
-
Worked examples
Small scenarios make a rule understandable and expose obvious mistakes. They teach the mechanism but cover only the cases chosen.
-
Implementation tests
Deterministic, adversarial, and integration tests exercise executable behavior. They are direct engineering evidence for the exact code and conditions tested.
-
Machine-checked theorems
A proof assistant checks a formal statement against explicit definitions and assumptions. The result covers the modeled state space, not every surrounding system.
-
Independent scrutiny
Review and security analysis challenge the model, assumptions, implementation, and deployment choices. A formal audit is a separate, named body of work with its own scope and result.
Lean checks every logical step
Lean is a proof assistant: a language for writing definitions, assumptions, theorem statements, and proofs in a form a small trusted checker can verify. If a proof step does not follow, the theorem does not check. That removes a large class of gaps that can hide in an informal argument.
People define the model boundary and connect it to executable behavior; the checker then verifies the logic inside that boundary. Astrea therefore states each theorem together with its assumptions and excluded layers.
What the checker establishes logic
The named conclusion follows from the formal definitions and assumptions in the checked source snapshot.
Outside the model the world
Networking, storage, deployment, hardware, operators, and the adversarial environment each require evidence at their own boundary.
These consensus excerpts come from a defined source version whose full imported proof set passed the checker. The result applies to that version. A changed theorem or dependency needs a fresh check; a Lean file by itself is not proof evidence.
Agreement receives the strictest treatment
The machine-checked theorem set focuses on Astrea's consensus core: the logic that establishes a compatible graph-final history under its stated Byzantine and network assumptions. Its safety results cover agreement properties such as quorum overlap and unique graph-final anchors. Its conditional liveness results cover bounded progress in the modeled windows, including disciplined round advancement and missing-parent repair.
The larger refinement chain connects the abstract consensus statements to a defined observable consensus-state boundary. The theorem ends at that boundary. Networking, storage, privacy routing, data availability, APIs, stake selection, and application behavior carry separate evidence.
Safety kernel: large voting sets must overlap
This compact excerpt is standard Byzantine quorum arithmetic. Under the theorem's premises, two quorum-sized signer sets overlap by more participants than the allowed faulty set. Larger safety results use that overlap to rule out conflicting graph-final anchors. The excerpt is one kernel lemma, not the entire consensus proof.
theorem quorum_intersection_cardinality (n f q cardA cardB cardInter : Nat) (hn : n = 3 * f + 1) (hq : q = 2 * f + 1) (hA : q ≤ cardA) (hB : q ≤ cardB) (hUnion : cardA + cardB ≤ n + cardInter) : f + 1 ≤ cardInter := by subst n subst q omega
Astrea's machine-checked mathematical proof covers the consensus core only. Networking, storage, privacy routing, data availability, APIs, stake selection, and application services are engineered and tested separately; testing is evidence, not a mathematical proof. The bridge's Zcash chain proof, beacon-chain import, private ledger, threshold signing, proxy execution, and settlement receipt belong to that engineered set, and the chains at either end keep their own guarantees.
Astrea closes a known liveness failure class
A Yale-led analysis by Longfei Qiu, Jingqi Xiao, and Zhong Shao found that Mysticeti liveness is sensitive to how honest participants advance rounds. If participants may jump over rounds arbitrarily, the paper constructs an infinite execution in which no data blocks are committed. Its corrected protocol restricts that behavior and restores liveness under the paper's model.
Astrea addresses the same failure class with its own disciplined advancement rule. An honest participant advances by one round, or uses an evidence-backed bounded skip that stays within the declared anchor and observation rules. An unsupported leap does not qualify.
Primary source: Qiu, Xiao, and Shao, “Mechanized Safety and Liveness Proofs for the Mysticeti Consensus Protocol under the LiDO-DAG Framework”, IEEE Symposium on Security and Privacy.
If round evidence satisfies Astrea's disciplined advancement predicate, that same evidence cannot describe an arbitrary round jump. This closes the exact jump condition. It does not, by itself, claim unconditional liveness for every network and deployment.
theorem selia_native_disciplined_rounds_exclude_arbitrary_jumps (evidence : RoundAdvanceEvidence) (hDiscipline : SeliaNativeRoundAdvanceDiscipline evidence) : ¬ ArbitraryRoundJump evidence
A complete proof claim names its boundary
A formal-verification claim is complete when it names the property, model, assumptions, checked source snapshot, and parts of the system outside the theorem.
Property
Safety, conditional liveness, deterministic ordering, or another exact result. One property does not silently imply the others.
Model
The states and transitions the theorem represents. Behavior absent from the model is not covered by the conclusion.
Assumptions
The Byzantine bound, committee conditions, network timing boundary, cryptographic premises, and other hypotheses needed by the result.
Lean check
The exact theorem source and imported dependencies accepted by the checker. Later edits require later evidence.
Scoped result
The exact conclusion, together with the networking, storage, privacy, availability, service, and deployment layers that remain outside it.
PixelVM has separately scoped mathematical statements, profile assumptions, and adversarial tests for its execution-and-proof architecture. The consensus theorem remains scoped to consensus; the two evidence paths make distinct claims.