Alpenglow Consensus Protocol - Formal Verification

This repository contains a comprehensive formal verification suite for the Solana Alpenglow consensus protocol, transforming the mathematical theorems from the whitepaper into machine-verified proofs using TLA+.

Whitepaper - https://drive.google.com/file/d/1Rlr3PdHsBmPahOInP6-Pl0bMzdayltdV/view?usp=drivesdk

Quick Start - Three Independent Verification Commands

This project provides three independent verification commands that can be run separately:

1. Correct Normal Model Verification (~13 minutes)

make verify-correct

• Purpose: Verify protocol safety and liveness with all correct nodes
• Configuration: AlpenglowCorrectNormalModelConfig.cfg (4 nodes, no Byzantine)
• Output: correct-normal-verification.log
• Tests: Fast path (80%) and slow path (60%) finalization under normal conditions

2. Byzantine Fault Tolerance Verification (~28 minutes)

make verify-byzantine

• Purpose: Verify protocol resilience against Byzantine adversaries
• Configuration: AlpenglowByzantineModelConfig.cfg (5 nodes, 1 Byzantine = 20%)
• Output: byzantine-verification.log
• Tests: Safety properties under equivocation, double voting, and malicious behavior

3. Formal Proof Verification (Variable time)

make verify-proofs

• Purpose: Verify mathematical proofs using TLAPS (TLA+ Proof System)
• Input: Alpenglow.tla specification with embedded proofs
• Output: proofs-verification.log
• Tests: Theorem 1 (Safety), lemmas, and mathematical correctness proofs

Run All Verifications (~50+ minutes)

make verify-all

Executes all three commands sequentially for complete verification coverage.

Direct TLC/TLAPM Commands

If you prefer to run the verification tools directly instead of using the Makefile:

1. Direct Correct Normal Verification

tlc --config AlpenglowCorrectNormalModelConfig.cfg Alpenglow.tla | tee correct-normal-verification.log

2. Direct Byzantine Verification

tlc --config AlpenglowByzantineModelConfig.cfg Alpenglow.tla | tee byzantine-verification.log

3. Direct Proof Verification

# Adjust path to your TLAPM installation
$HOME/Downloads/tlapm/bin/tlapm Alpenglow.tla
# Or if installed system-wide:
tlapm Alpenglow.tla

Note: These direct commands require:

• TLA+ tools (tla2tools.jar) in your classpath or tlc command available
• TLAPM installed for proof verification
• Sufficient Java heap memory (add -Xmx12g to tlc if needed)

Project Structure

├── Alpenglow.tla                           # Main TLA+ specification (1611 lines)
├── AlpenglowCorrectNormalModelConfig.cfg   # Normal operation config (4 nodes)
├── AlpenglowByzantineModelConfig.cfg       # Byzantine testing config (5 nodes, 1 Byzantine)
├── Makefile                                # Build automation with three main targets
├── correct-normal-verification.log         # Output from verify-correct
├── byzantine-verification.log              # Output from verify-byzantine  
├── proofs-verification.log                 # Output from verify-proofs
└── states/                                 # TLC state exploration results

What Gets Verified

✅ Safety Properties (All Three Commands)

• Theorem 1: No conflicting blocks finalized in same slot
• Chain Consistency: Proper block ancestry under Byzantine faults
• Certificate Uniqueness: At most one notarization per slot
• Non-Equivocation: No double finalization certificates

⚡ Liveness Properties (verify-correct, verify-byzantine)

• Fast Path: One-round finalization with 80% stake
• Slow Path: Two-round finalization with 60% stake
• Progress Guarantee: Advancement under partial synchrony
• Bounded Time: min(δ₈₀%, 2δ₆₀%) finalization bound

Byzantine Resilience (verify-byzantine specifically)

• 20% Byzantine Tolerance: Safety with up to 20% malicious stake
• Equivocation Detection: Double voting and conflicting block tracking
• Network Partition Recovery: Continued progress after partition healing

Mathematical Proofs (verify-proofs specifically)

• Theorem 1 (Safety): Formal mathematical proof
• Supporting Lemmas: Lemma 7 (Rotor resilience), Lemmas 20-42
• Definition Consistency: Verification of Definition 16 (SafeToNotar/SafeToSkip)

Prerequisites & Installation

System Requirements

• Java 11+ (for TLA+ tools)
• Python 3.7+ (optional, for analysis scripts)
• 12+ GB RAM recommended for large model verification

Installation

# Install TLA+ tools automatically
make install-deps

# Manual installation:
# Download from https://github.com/tlaplus/tlaplus/releases
# For TLAPS: https://github.com/tlaplus/tlapm/releases

Quick Syntax Check

make syntax-check

Verification Results Summary

Command	Configuration	Nodes	Byzantine	Runtime	Properties Verified
verify-correct	CorrectNormal	4	0 (0%)	~13 min	Safety + Liveness
verify-byzantine	Byzantine	5	1 (20%)	~28 min	Safety + Byzantine Resilience
verify-proofs	Mathematical	N/A	N/A	Variable	Formal Proofs

Results

CorrectNormalModelConfig

ByzantineModelConfig

Documentation & Resources

• TLA+ Specification: Complete formal model (1611 lines)
• Configuration Files:
  • AlpenglowCorrectNormalModelConfig.cfg - Normal operation parameters
  • AlpenglowByzantineModelConfig.cfg - Byzantine testing parameters

Acknowledgments

• Solana Labs: Original Alpenglow protocol design
• Alpenglow Authors: Quentin Kniep, Jakub Sliwinski, Roger Wattenhofer
• Leslie Lamport: TLA+ specification language
• TLA+ Community: Model checking tools and methodology