GOAT Network Publishes BitVM3 Model Checking Results
A GOAT Network blog post details a TLA+ model checking exercise on the GOAT BitVM3 bridge ahead of mainnet.
goat.network/news
🔗
Model checking the GOAT BitVM3 bridge
We model checked the GOAT BitVM3 bridge in TLA+. 8 findings, all fixed and re-verified, every counterexample published, 2 items still open.
Every spec was built from the Rust source rather than the documentation, which surfaced 3 places where the docs had drifted from the code.