Model checking a live blockchain bridge with Specl
I built Specl, a specification language and model checker for concurrent and distributed systems. This post demonstrates its practical value by model checking the protocol behind a live blockchain bridge that I helped build while working at Dymension.
The bridge moves KAS tokens between the Kaspa and Dymension blockchains. It is live and has processed real funds. The full design is published on the Dymension forum and the escrow address is visible on the Kaspa explorer.
The bridge protocol
The bridge has four components: the Kaspa chain, the Dymension Hub chain, an untrusted relayer and a trusted validator set. The relayer brings liveness by being proactive. The validator set brings safety by verifying everything and providing signatures. The relayer is entirely untrusted: it does not control funds.
There are two directions: deposits (Kaspa to Hub) and withdrawals (Hub to Kaspa).
Deposits are straightforward. A user sends KAS to a multisig escrow address on Kaspa. The relayer notices, constructs a minting transaction for the Hub, gathers validator signatures and submits it. The Hub stores the deposit's outpoint in a seen-set and mints wrapped KAS. The seen-set prevents replay: each outpoint is credited exactly once.
Withdrawals are harder. A user burns wrapped KAS on the Hub, creating a withdrawal request in a queue. The relayer constructs a Kaspa transaction to release escrowed KAS. The transaction must spend a designated anchor UTXO stored in the Hub's state. The validator signs only if the anchor is live and the withdrawal range advances monotonically. After Kaspa accepts the transaction, the relayer brings a confirmation back to the Hub, which does a compare-and-set to update the anchor and mark the withdrawals as complete.
The anchor chain mechanism is the core insight. Each Kaspa withdrawal transaction spends the previous anchor and creates a new one, forming a sequential chain. Because a UTXO can only be spent once, this makes double-spending impossible: you can't create two valid transactions from the same anchor.
The Hub maintains two pieces of bookkeeping state:
- O: the current anchor outpoint (a pointer to the UTXO that must be spent next)
- L: the index of the last withdrawal confirmed as bridged to Kaspa
The protocol guarantees the peg: escrowed KAS and minted wKAS are always in 1:1 correspondence.
Why model check?
The protocol has a manually written safety proof in the design document. But proofs about concurrent systems are notoriously easy to get wrong. The interleaving of message loss, replay, reordering and adversarial relayer behaviour creates a combinatorial space that is hard to reason about exhaustively by hand.
Model checking explores every reachable state. If there's a violating trace, it finds it and shows you. If it doesn't find one, you know the property holds for all interleavings up to the bound you checked.
Model checking also enables mutation testing: systematically removing safety checks from the protocol and verifying that the model detects the resulting vulnerability. If removing a critical check doesn't break any invariant, your specification is too weak. This is how you build genuine confidence, rather than just confirming that a correct model is correct.
Why Specl?
Specl is a TLA+ alternative designed to be more accessible. It uses familiar programming language syntax (no learning the TLA+ math typesetting) while preserving the full power of model checking. The same protocol that might take 200 lines of TLA+ takes about 100 lines of Specl, and reads like pseudocode.
For this bridge protocol, the Specl model has 8 actions, 8 invariants and when parameterized with N=6 it is checked in 45 seconds:
Result: OK
States explored: 69.14M
Max depth: 54
Time: 44.8s
Throughput: 1.54M states/s
Optimizations: POR, fast
The Specl model
The model has 13 state variables organized into five groups:
Hub chain state: the anchor hub_O, last confirmed index hub_L, withdrawal queue length hub_queue, deposit seen-set hub_seen, and a mint counter hub_minted.
Kaspa chain state: the set of unspent transaction outputs unspent, a monotonic UTXO ID allocator next_id, and the escrow balance escrow.
Messages: signed_withdrawals and executed_withdrawals are persistent (the relayer always has signed data; executed transactions are on-chain). Deposit messages deposit_msgs can be dropped.
User state: deposits, the set of deposit outpoints that exist on Kaspa.
Ghost state: released tracks which withdrawal indices have had funds released on Kaspa. This is not part of the protocol state but allows writing invariants about the relationship between Kaspa releases and Hub bookkeeping.
The 8 actions model every step of both directions:
UserDeposit -> user sends KAS to escrow
RelayDeposit -> relayer observes and forwards deposit
HubCredit -> Hub credits wrapped KAS (anti-replay via seen-set)
UserWithdraw -> user burns wKAS, creating a withdrawal request
ValidatorSignWithdrawal -> validator signs a Kaspa TX (checks anchor, L, escrow)
KaspaExecute -> Kaspa executes a signed TX (UTXO uniqueness)
HubConfirm -> Hub confirms execution (compare-and-set on O)
DropDepositMsg -> adversarial relayer drops a deposit message
Withdrawal messages are encoded as [spend, create, from_L, target_L]: which UTXO to spend, which to create, and the range of withdrawal indices being processed.
Signed withdrawals are not consumed when executed. The relayer always has the signed data and can attempt replay. Kaspa's UTXO uniqueness rule is the sole mechanism preventing double-execution. This is a deliberate modeling choice: the adversary gets every possible advantage.
The invariants
The model checks 8 invariants:
| Invariant | Property |
|---|---|
| NoUnauthorizedRelease | Every released index is a valid withdrawal request |
| DepositIntegrity | Hub never credits a nonexistent deposit |
| HubLBounded | Confirmed index never exceeds queue length |
| PegWithdrawalSafety | Can't release more withdrawals than requested |
| PegDepositSafety | Can't credit more deposits than made |
| EscrowNonNegative | Escrow never goes negative |
| PegBalance | escrow == 1 + deposits - releases (exact accounting; the 1 is the seed UTXO) |
| NoDoubleMint | Every HubCredit corresponds to a unique deposit |
Mutation testing
To validate the model's sensitivity, I removed each safety check one at a time and re-ran the model checker. The question: does the model detect the resulting vulnerability?
The protocol has 7 require guards across its actions. Each guard was commented out individually:
| # | Guard removed | Location |
|---|---|---|
| M1 | msg[0] in unspent (UTXO uniqueness) | KaspaExecute |
| M2 | msg[0] == hub_O (compare-and-set) | HubConfirm |
| M3 | hub_L < target_L (L monotonicity) | ValidatorSignWithdrawal |
| M4 | not (id in hub_seen) (anti-replay) | HubCredit |
| M5 | hub_O in unspent (anchor is live) | ValidatorSignWithdrawal |
| M6 | escrow >= target_L - hub_L (escrow sufficiency) | ValidatorSignWithdrawal |
| M7 | hub_L < msg[3] (L check) | HubConfirm |
Results
| # | Guard removed | Result | Invariant violated | Role |
|---|---|---|---|---|
| M1 | UTXO uniqueness | FAIL | EscrowNonNegative | Safety |
| M2 | Compare-and-set | PASS | -- | Liveness |
| M3 | L monotonicity | FAIL | PegBalance | Safety |
| M4 | Anti-replay | FAIL | NoDoubleMint | Safety |
| M5 | Anchor is live | PASS | -- | Liveness |
| M6 | Escrow sufficiency | FAIL | EscrowNonNegative | Safety |
| M7 | L check (hub confirm) | PASS | -- | Liveness |
All 4 safety-critical guards are detected when removed. The 3 guards that pass are correctly classified as (psuedo) liveness or optimization mechanisms: their removal doesn't break the peg, but can stall progress, i.e. break the bridge without stealing money.
The counterexamples
M1 (no UTXO uniqueness): the same signed withdrawal executes twice on Kaspa, draining escrow below zero.
M3 (no L monotonicity): the validator signs a backward withdrawal range where target_L < hub_L. When target_L - hub_L is negative, escrow -= (target_L - hub_L) increases escrow without any deposit. The peg breaks. This is subtle: the existing escrow >= target_L - hub_L guard doesn't catch it because the right-hand side is negative, so the guard trivially holds. Only the exact PegBalance invariant detects the inflation.
M4 (no anti-replay): the same deposit gets credited repeatedly. The hub_seen set doesn't grow (sets are idempotent under union), which is why you need a separate hub_minted counter to detect it.
M6 (no escrow sufficiency): two withdrawals with no deposits drain escrow below zero.