GOAT Network's BitVM bridge implementation connects Bitcoin and GOAT L2 through presigned transaction graphs, optimistic verification, and proof-based disputes. See the GOAT BitVM Whitepaper for protocol background.

Open the full-size graph for peg-in, Operator claims, Watchtower and Verifier challenges, timeouts, and PreKickoff paths. Blue lines show Operator and claim transactions; red lines show challenges and timeouts. Dots join branches; crossings without dots do not.

• Node — roles and execution
• Circuits — proof composition and compatibility
• Proof Builder — proof coordination and recovery
• Deployment — running bridge participants
• Localnet — local testing
• End-to-end checks — protocol and fault scenarios
• Operator tools — read-only diagnosis

Rust tests check connector wiring, competing spends, and CSV values. TLA+ models check timing and core dispute safety, including invalid assertions, unpublished public inputs, and late assertions after Connector F has matured.

make tla-setup
cargo test -p bitvm-gc --test transaction_graph_invariants --test tla_shipped_values
make tla

After changing timing constants, run make tla-values before checking the models. Every model-checking failure fails CI. These checks rely on bounded response assumptions and do not establish end-to-end bridge safety or liveness; fees, relay policy, reorgs, cryptography, and contract settlement need separate review.

Open an issue or pull request with a concrete problem, proposed change, and relevant validation.