<h2 class="heading-node">Overview</h2>Alpenglow is Solana's consensus protocol upgrade achieving dramatic improvements over TowerBFT:<ul class="list-node"><li>100-150ms finalization (100x faster than current)</li><li>Dual-path consensus: Votor enables fast finalization with 80% stake participation or conservative finalization with 60% stake</li><li>Optimized block propagation: Rotor uses erasure coding for efficient single-hop block distribution</li><li>"20+20" resilience: Tolerates up to 20% Byzantine nodes plus 20% crashed/offline nodes under good network conditions</li></ul>Despite rigorous academic design, Alpenglow currently has only paper-based mathematical proofs. For a blockchain securing billions in value, we need machine-checkable formal verification.<h2 class="heading-node">The Challenge</h2>Transform the mathematical theorems from the Alpenglow whitepaper into proofs using formal methods tools (TLA+ or Stateright). You must create abstract formal models and prove correctness properties in the paper.<h2 class="heading-node">Key Requirements</h2><h3 class="heading-node">1. Complete Formal Specification</h3><ul class="list-node"><li>Protocol modeling in TLA+ or Stateright covering:<ul class="list-node"><li>Votor's dual voting paths (fast 80% vs slow 60% finalization)</li><li>Rotor's erasure-coded block propagation with stake-weighted relay sampling</li><li>Certificate generation, aggregation, and uniqueness properties</li><li>Timeout mechanisms and skip certificate logic</li><li>Leader rotation and window management</li></ul></li></ul><h3 class="heading-node">2. Machine-Verified Theorems</h3>Safety Properties:<ul class="list-node"><li>No two conflicting blocks can be finalized in the same slot</li><li>Chain consistency under up to 20% Byzantine stake</li><li>Certificate uniqueness and non-equivocation</li></ul>Liveness Properties:<ul class="list-node"><li>Progress guarantee under partial synchrony with &gt;60% honest participation</li><li>Fast path completion in one round with &gt;80% responsive stake</li><li>Bounded finalization time (min(δ₈₀%, 2δ₆₀%) as claimed in paper)</li></ul>Resilience Properties:<ul class="list-node"><li>Safety maintained with ≤20% Byzantine stake</li><li>Liveness maintained with ≤20% non responsive stake</li><li>Network partition recovery guarantees</li></ul><h3 class="heading-node">3. Model Checking &amp; Validation</h3><ul class="list-node"><li>Exhaustive verification for small configurations (4-10 nodes)</li><li>Statistical model checking for realistic network sizes</li></ul><h2 class="heading-node">Deliverables</h2>GitHub Repository:<ul class="list-node"><li>Complete formal specification</li><li>All proof scripts with reproducible verification results</li><li>Submission must be original work and open-source under Apache 2.0</li></ul>Technical Report and Video Walkthrough:<ul class="list-node"><li>Executive summary of verification results</li><li>Detailed proof status for each theorem and lemmas</li></ul><h2 class="heading-node">Evaluation Criteria</h2><ul class="list-node"><li>Rigor: Successfully verify or refute core theorems with proper formal abstraction</li><li>Completeness: Comprehensive coverage including edge cases and boundary conditions </li></ul>Disclaimer: We reserve the right to adjust prize distribution based on the quality of submission: (1) If no submission meets our minimum standards, no prizes will be awarded; (2) If we receive submissions but they do not meet the quality we expect, we may reduce prize amounts or distribute them as individual bonus prizes<h2 class="heading-node">Resources</h2><ul class="list-node"><li><a class="link" href="https://drive.google.com/file/d/1Rlr3PdHsBmPahOInP6-Pl0bMzdayltdV/view">Alpenglow Whitepaper</a>&nbsp;</li><li><a class="link" href="https://disco.ethz.ch/members/wroger/AlpenglowPresentation.pdf">Accelerate Alpenglow Presentation Slides</a></li><li><a class="link" href="https://www.anza.xyz/blog/alpenglow-a-new-consensus-for-solana">Alpenglow: A New Consensus for Solana</a></li><li><a class="link" href="https://www.helius.dev/blog/alpenglow">Solana’s Great Consensus Rewrite</a></li><li><a class="link" href="https://github.com/qkniep/alpenglow/tree/main">Alpenglow Reference Implementation</a></li><li><a class="link" href="https://www.helius.dev/blog/consensus-on-solana">Consensus on Solana</a></li><li><a class="link" href="https://youtu.be/x1sxtm-dvyE?si=4rsTKAcEuwn8Xcds">Scale or Die at Accelerate 2025: Introducing Alpenglow - Solana’s New Consensus</a></li><li><a class="link" href="https://www.stateright.rs/title-page.html">Stateright</a></li><li><a class="link" href="https://learntla.com/core/index.html">TLA+</a></li></ul>

Formal Verification of Solana Alpenglow Consensus Protocol

Formal Verification of Solana Alpenglow Consensus Protocol

10kUSDC Total Prizes
10k USDC 1st