Skip to content

README.md

Latest commit

 

History

History
215 lines (134 loc) · 6.62 KB

README.md

File metadata and controls

215 lines (134 loc) · 6.62 KB
Raw

Solana Alpenglow - Formal Verification

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.

Votor's dual voting paths - Coverage

alt text

Flow Diagrams

System Overview

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

alt text

State Transitions

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)

alt text

Mathematical Foundations

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)

alt text



Rotor's erasure-coded block propagation - Flow Diagrams

Shows: 3-phase process (Leader→Relays→Nodes→Reconstruction)

image

Rotor overview (One To One)

  • 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)

alt text

alt text

To Test Byzantine Behavior: Change your config to:

CONSTANTS
    MaxFailures = 1    (* Allow 1 Byzantine node *)

Rotor overview (One To Many)

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.

alt text

alt text

To Test Byzantine Behavior: Change your config to:

CONSTANTS
    MaxFailures = 1    (* Allow 1 Byzantine node *)

Rotor overview (Many To Many)

  • 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.

alt text

alt text

To Test Byzantine Behavior: Change your config to:

CONSTANTS
    MaxFailures = 1    (* Allow 1 Byzantine node *)



Certificate generation - Coverage

alt text

Flow Diagrams

System Overview Diagram

  • 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)

alt text

State Transition Diagram

  • 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

alt text



Timeout mechanisms and skip certificate logic - Coverage

alt text

Flow Diagrams

Alpenglow Timeout Flow

  • Purpose: Complete end-to-end process visualization
  • Shows: Timeout detection → skip voting → certificate generation
  • Includes: Verification results (12,246 TimeoutTrigger actions), stake tables, timeline

alt text

State Machine

  • Purpose: Clean state transition logic
  • Shows: Consensus states from init → timeout → skip → certificate
  • Includes: Normal voting path vs timeout path, Byzantine behavior integration

alt text

Byzantine Network Model

  • 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

alt text



Leader rotation and window management - Coverage

alt text

Flow Diagram

LeaderRotation System Overview

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.

alt text