Before mainnet, we ran a formal verification round on the GOAT bridge node. The full report is public, including the counterexamples, the fixes, what the audit itself got wrong on the way, and what is still open. This page exists for one reason: to make it as easy as possible for you to check our work and tell us what we missed.
Report: github.com/GOATNetwork/bitvm2-node/blob/gc-v2/audit/TLAPlus-20260710.md
Specs: github.com/GOATNetwork/bitvm2-node/tree/gc-v2/node/tla
What was verified, and what was not
The round modeled three things in TLA+ and checked them exhaustively with TLC: the bridge node's status bookkeeping (the local database state machines), the peg-out transaction graph's timelock configuration, and the shared Taproot connectors where competing transactions race for the same UTXO. Every spec was built from the Rust source rather than the documentation, which surfaced 3 places where the docs had drifted from the code. Those are corrected.
The boundary matters as much as the coverage. These models do not re-derive Bitcoin consensus; a single-spend UTXO is trusted as a primitive. They also do not check transaction wiring, fee conservation, or the Taproot leaf scripts themselves. The report names these as candidates for a follow-up round, and they are open territory if you want them.
What was found
8 real issues. 7 came with machine-checked counterexamples produced from shipped configuration values, not injected test cases. The eighth was a read-then-write staleness bug caught during modeling and fixed at code level. Most were races between uncoordinated writers to the same status row in the node's local database. Two were timelock margin gaps in the transaction graph itself.
None were fund-custody bugs, and we want to be precise about that in both directions. Bitcoin's UTXO model decides the real on-chain outcome regardless of these bugs, and the L2 contract's own status guards were verified directly against Gateway.sol. What could drift was the node's local record of on-chain outcomes. The margin findings were sharper: on testnet4, the shipped values put Disprove's and Take2's earliest-spendable heights on the exact same block, turning the honest path's win into a coin flip on mempool ordering. TLC found that on its first run. The fix landed with a margin of 8 blocks, and the models were re-run against the new shipped numbers.
The round also cleared three things it went looking for. The one that matters most: 1-of-N holds. Any single watchtower or verifier, acting alone on its own timing, permanently denies a cheating operator's claim. That was checked with independent actors across all 4 networks, 1,618,897 states, zero violations.
What is fixed and what is not
All 8 findings are fixed in commit 991faaa. The fixes were written independently by the team, and each was re-verified against the audit's own models using the actual shipped values, not the originally proposed ones. In several cases the shipped fix is stronger than the audit's proposal, and the report says so per finding.
2 smaller, lower-priority defects remain open. They are documented under Finding 8 with file and line. We are publishing them anyway, and they are a reasonable place to start a review.
How to check our work
Every spec and config lives in node/tla/ with a table in the repo README. Any of them runs locally:
cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config <Spec>.cfg <Spec>.tla
CI runs the full set on every push. The pre-fix bug configs are deliberately kept as a permanent historical record: the job fails only if one of their frozen counterexamples unexpectedly stops reproducing, which would mean either a guard was silently removed or a spec stopped demonstrating what it claims.
What we are asking for
We’re seeking security-relevant feedback. Concretely:
Re-run the specs and challenge the models themselves, including the scope boundary. Extend the multi-actor model to Byzantine actors or to more than 2 watchtowers and verifiers; the report proposes exactly this. Take on the follow-up territory the models deliberately excluded: transaction wiring, value conservation, leaf-script authorization. Pick up the 2 open items. Or attack the running system directly: the deployment guide covers building the node and configuring any of its roles, including Challenger and Watchtower, the two roles whose entire job is catching a misbehaving operator. The node README documents the architecture, state machines, and RPC API. GOAT testnet chain RPC: https://rpc.testnet3.goat.network
File anything you find as an issue: https://github.com/GOATNetwork/bitvm2-node/issues
