Wormhole VAA TLA+ Verification

This project contains TLA+ specifications to model and check safety and correctness properties of a Wormhole node processing VAAs.

Modules

1️⃣ BroadcastStorage.tla

Models a very simple system with:

• broadcasting a VAA
• storing it
• redeeming it
• node crash / restart behavior

It checks that the system never reaches a state where a VAA is:

• broadcast
• not stored
• but redeemed anyway

2️⃣ WormholeVAAProcessor.tla

Models a more detailed Wormhole node with:

• guardian signatures
• quorum logic
• gossip capacity
• memory vs persistent storage
• crash and recovery
• vulnerable vs correct behavior paths

It includes safety invariants and basic liveness checks, such as:

• consistency between broadcast and storage
• durability across crashes
• memory matching persistent DB after recovery
• eventual broadcast and persistence

How to Run

You can run using TLA+ Toolbox or the CLI.

Using Toolbox

1. Open the .tla file
2. Create a model
3. Set Spec as the specification
4. Add invariants / properties to check
5. Run model checking

CLI

tlc2 BroadcastStorage.tla

or

tlc2 WormholeVAAProcessor.tla

Notes

• These specs are simplified models
• Designed for experimenting, debugging behavior, and checking safety assumptions

---