Alpenglow Verifier

Counterexample Analysis

An interactive tool to analyze and debug model checking violations.

✅ Byzantine Double Voting Vulnerability Fixed

The Byzantine double voting issue identified in counterexample analysis has been successfully resolved. The CanFinalize function now only counts honest stake toward finalization quorum, preventing Byzantine nodes from compromising safety.

Property Violated (Historical) NoConflictingBlocksFinalized

This counterexample shows the original vulnerability before the fix was applied.

State Trace

Step-by-step execution leading to failure.

State at Step 1

nodes	[ { "id": 1, "status": "idle", "stake": 25, "currentSlot": 1, "votes": {} }, { "id": 2, "status": "idle", "stake": 25, "currentSlot": 1, "votes": {} }, { "id": 3, "status": "idle", "stake": 25, "currentSlot": 1, "votes": {} }, { "id": 4, "status": "byzantine", "stake": 20, "currentSlot": 1, "votes": {} } ]
messages	[]
finalized	{}
certs	[]
skip_certs	[]
leader	1
slot	1
current_time	0

Protocol Visualization

Visual state of the network at step 1.

AI-Powered Explanation

Analyze the counterexample and get a suggested fix.

Click "Get Explanation" to see the AI analysis.