Many proposals.
One shared history.

Mysticeti, hardened and narrowed

Astrea did not invent consensus from a blank page. The core is built on Mysticeti, the DAG consensus design created for Sui, and it was chosen for one reason: speed. Validators propose in parallel instead of taking turns, and the protocol commits directly from the graph without extra certification rounds, so agreement arrives within a few message delays. Astrea then changed the design in three ways.

First, the fix. A consensus can be perfectly safe and still stop deciding. A Yale-led mechanized analysis of Mysticeti constructed exactly that run: when participants may leap ahead over rounds without justification, the graph keeps growing while commitment never happens — blocks are produced forever, and none of them is ever finalized. Astrea's advancement rule closes that door. A validator moves one round at a time, or takes a bounded skip backed by explicit evidence, and a machine-checked theorem confirms the arbitrary jump is excluded. The full account and the named Lean result are below.

Second, native trace-monoid concurrency. Most consensus designs order everything, then let execution engines guess what could have run in parallel. Astrea builds the independence rules into the protocol itself: registered rules declare when two operations provably cannot interfere, and only then may they swap or run side by side. Ordering effort goes where ordering matters; everything else moves concurrently without changing the result.

Third, the narrowest acceptance rule we could write. Where the protocol requires computation, consensus accepts exactly one form of evidence: a zkCHARK receipt. Not a re-execution, not a trusted operator's word, not an alternative proof format — a zero-knowledge receipt or nothing. One format means one verifier to build, review, and harden; a hot path that stays small because it only ever checks; and privacy by construction, because the only evidence consensus ever sees is the kind that keeps private inputs private.

That last change is also an energy decision. Checking a receipt costs a small, bounded amount of work; re-executing costs whatever the program cost, again, on every machine that wants to trust the result. Under repetition, the network's total compute bill is one execution per participant. Under verification it stays close to one execution, full stop — so adding validators buys more security without multiplying the work.

A graph becomes one history

Validators publish proposals concurrently and link each proposal to earlier ones they have seen. Astrea builds those references into a graph and applies a deterministic rule that every honest participant can use to derive the same authoritative history.

A validator is a participant authorized to check and propose protocol objects. During an epoch, the authorized validators and their voting weights form a committee. A quorum provides enough voting weight to make a protocol decision despite the model's bounded faulty minority.

Delivery starts the path to finality

Arrival triggers validation rather than authority. Astrea checks the object and its parent relationships before accepting it. A valid object with a missing parent waits in a bounded staged state while repair catches up.

Global agreement is reserved for authority

Every job inside consensus must be repeated and coordinated by the validator set, so the verification operating system keeps that shared loop small. Authority stays stable while the specialized systems around it stay free to improve.

The hot path is the short sequence every validator must complete to advance authoritative history. It validates the protocol object, checks its parents and registered commitments or receipts, applies consensus rules, and extends the committed order.

Parallelism follows meaning

The comparison starts from one base snapshot: the exact named version of state both actions are evaluated against. Two actions have semantic independence when registered rules establish that neither interferes with the other at that snapshot and either legal order preserves the same meaning.

The technical model is a trace monoid: a sequence of actions can be rearranged only through declared swaps of independent neighbors. A shard owns or processes a partition of state or work. A lane is an ordered execution path within that routing plan. The independence rules determine which actions may move between lanes without changing the result.

A hot key is state touched by enough dependent actions that their order matters. Astrea gives that work a clear serial path. Cross-shard operations carry explicit coordination rules, while migration moves ownership at a declared boundary. Extra shards create room only for work that the registered independence rules already separate.

Three kinds of composition

Three composition mechanisms solve three separate problems: scheduling independent transactions, reducing ordered proof chunks, and producing a compact receipt.

Round advancement has a hard boundary

Liveness means the protocol continues making decisions under its stated network and fault assumptions. In a Yale-led mechanized analysis of Mysticeti, the researchers construct an infinite execution where arbitrary round jumping prevents data blocks from committing. Their model regains liveness when that behavior is restricted.

Primary source: Longfei Qiu, Jingqi Xiao, and Zhong Shao, “Mechanized Safety and Liveness Proofs for the Mysticeti Consensus Protocol under the LiDO-DAG Framework”. The paper analyzes Mysticeti; Astrea's correction and theorem below belong to Astrea's own consensus model.

Machine-checked safety and progress

Replacing trust with proof applies to the ordering rule itself. Astrea's Lean model machine-checks consensus safety and conditional liveness under explicit assumptions: the safety result excludes conflicting committed histories, and the liveness result establishes progress when the stated fault, network, and round-advancement conditions hold.

Safety: one slot cannot acquire two graph-final roots

A graph-final certificate represents the committee's decision for one position in history. The checked kernel below says two such certificates cannot bind different roots when their signer overlap exceeds the faulty bound and only faulty validators could have signed both conflicting roots.

theorem single_slot_graph_final_anchor_uniqueness
    {Root : Type} [DecidableEq Root]
    (rootA rootB : Root)
    (f cardInter byzantineInInter : Nat)
    (hIntersection : f + 1 ≤ cardInter)
    (hByzantineBound : byzantineInInter ≤ f)
    (hDifferentImpliesOnlyByzantine :
      rootA ≠ rootB → cardInter ≤ byzantineInInter) :
    rootA = rootB

Safety across epochs: one anchor determines one next roster

Reconfiguration changes the committee without creating a second source of history. This theorem checks that two valid handoff views tied to the same anchored prefix derive the same next roster root.

theorem L_RECONF_same_anchor_same_roster
    (deriveRoster : Nat → Nat)
    (deriveGenesis : Nat → Nat → Nat)
    (left right : EpochHandoff α)
    (hLeft : ValidHandoff deriveRoster deriveGenesis left)
    (hRight : ValidHandoff deriveRoster deriveGenesis right)
    (hSameAnchor :
      left.anchoredPrefixDigest = right.anchoredPrefixDigest) :
    left.rosterRoot = right.rosterRoot

theorem selia_native_disciplined_rounds_exclude_arbitrary_jumps
    (evidence : RoundAdvanceEvidence)
    (hDiscipline : SeliaNativeRoundAdvanceDiscipline evidence) :
    ¬ ArbitraryRoundJump evidence

Conditional liveness: supported work reaches a commit bound

The larger progress result follows a valid handoff into the next epoch. Given a stable prefix, bounded catch-up, synchronized good rounds, an online fairly scheduled committee, supported honest-anchor evidence, and execution of the commit rule, the opened epoch commits that supported anchor within its declared finite window.

theorem
    llive5_reconfiguration_opened_epoch_supported_anchor_commits_within_bound
    {α : Type u}
    (deriveRoster : Nat → Nat)
    (deriveGenesis : Nat → Nat → Nat)
    (model : LLive0Model)
    (c : Nat)
    (window : OpenEpochReconfigurationWindow α)
    (hAssumptions :
      LLive5ReconfigurationAssumptions
        deriveRoster deriveGenesis model c window) :
    OpenedEpochSupportedAnchorCommitsWithinBound
      deriveRoster deriveGenesis model c window

Next · PixelVM proves execution → ← Astrea Tech