Formal verification of Solana's Alpenglow consensus protocol using TLA+ specification language, focusing on the Votor's dual voting paths, Rotor's erasure-coded block propagation, Certificate generation, Timeout mechanisms and skip certificate logic, Leader rotation and window management mechanism described in the Alpenglow whitepaper.
What it shows: The complete dual voting architecture
- 5 nodes with different stake percentages (25%, 25%, 25%, 15%, 10%)
- Fast Path (green): 80% stake → single round finalization
- Slow Path (orange): 60% stake → two-round finalization
- Concurrent execution where whichever path completes first wins
- Byzantine fault tolerance and safety/liveness properties
What it shows: The formal state machine flow
- States: Init → Propose → Vote → Threshold → Finalize
- Two parallel paths converging to final block finalization
- Error conditions (Byzantine attacks, timeouts)
- Integration with Global Stabilization Time (GST)
What it shows: The theoretical basis and formal verification
- Paper assumptions (Byzantine <20%, partial synchrony)
- Main theorems: Safety (Theorem 1) and Liveness (Theorem 2)
- Mathematical formulas for stake calculations and thresholds
- Safety properties (chain consistency) and liveness properties (eventual finalization)
Shows: 3-phase process (Leader→Relays→Nodes→Reconstruction)
- Shows: 3-phase process (Leader→Relays→Nodes→Reconstruction)
- Visualizes shred generation (4 shreds), relay assignments, and reconstruction
- Includes network timing (Delta=1, TimeAdvance<210) and thresholds (≥2 shreds needed)
To Test Byzantine Behavior: Change your config to:
CONSTANTS
MaxFailures = 1 (* Allow 1 Byzantine node *)
Setup: 1 Leader + 2 Relays + Multiple Network Nodes
Strategy:
- Critical shreds (1,4) → sent to BOTH relays (redundancy)
- Normal shreds (2,3) → sent to ONE relay each (efficiency)
Result:
- Only 6 messages instead of 8 (25% savings)
- Maintains fault tolerance with critical edge protection
- Uses Reed-Solomon coding with minimum 2 shreds for reconstruction
Key benefit: Smart selective redundancy - protect what's critical, optimize what's not.
To Test Byzantine Behavior: Change your config to:
CONSTANTS
MaxFailures = 1 (* Allow 1 Byzantine node *)
- Leader generates 4 shreds (erasure-coded block pieces)
- Each shred goes to ALL relays (many-to-many distribution)
- 2 relays forward everything to network nodes
- Any 2 shreds can reconstruct the complete block
Key insight: Higher fault tolerance but 2× bandwidth cost compared to one-to-one relay.
Numbers: 8 SHRED messages + 24 RELAY_SHRED messages for a 3-node network with 4 shreds.
To Test Byzantine Behavior: Change your config to:
CONSTANTS
MaxFailures = 1 (* Allow 1 Byzantine node *)
-
Purpose: Complete visual map of the Alpenglow consensus protocol
-
Key Elements:
- System Components: Nodes, Slots, Blocks, and Stakes
- 5 Vote Types: NotarVote, SkipVote, NotarFallbackVote, SkipFallbackVote, FinalVote
- 5 Certificate Types: FastFinalizationCert (≥80%), NotarizationCert (≥60%), NotarFallbackCert, SkipCert, FinalizationCert
- 2 Finalization Paths: Fast (direct) and Slow (conditional)
- Purpose: Shows protocol flow from voting to finalization
- Key Flow: Initial State → Voting → Certificate Generation → Finalization → Final State
- Highlights: Vote thresholds, feedback loops, and safety constraints
- Purpose: Complete end-to-end process visualization
- Shows: Timeout detection → skip voting → certificate generation
- Includes: Verification results (12,246 TimeoutTrigger actions), stake tables, timeline
- Purpose: Clean state transition logic
- Shows: Consensus states from init → timeout → skip → certificate
- Includes: Normal voting path vs timeout path, Byzantine behavior integration
- Purpose: Network topology and fault tolerance
- Shows: Node roles (80% honest, 20% Byzantine), message flows, attack scenarios
- Includes: Threshold analysis (50% skip, 60% notarization), safety invariants
What it shows: Visual map of Solana's leader rotation consensus protocol
Key parts:
- Windows: Groups of 4 slots per leader
- Flow: Activate window → Produce blocks → Finalize → Handoff
- Safety: One leader per slot, no overlaps
- Timeouts: Dynamic extensions when network stalls
- Main insight: Shows how validators take turns producing blocks in organized windows while handling failures gracefully.
