Verifying Consensus Protocols from LLM-assisted TLA$^+$: A Case Study of Byzantine Reliable Broadcast

TLA$^+$ (Temporal Logic of Actions) is a formal specification language well-suited for distributed systems. However, writing proper TLA$^+$ scripts requires high domain expertise. When it comes to modeling Byzantine behaviors for Byzantine fault-tolerant consensus protocols, the simulation of malicious behavior is a fundamental challenge: overly simplified modeling misses critical vulnerabilities, and verbose modeling leads to state-space explosion.

In this paper, we present TLAssist, a large language model (LLM)-assisted tool for semi-automated TLA$^+$ generation tailored for Byzantine reliable broadcast (RBC) protocols. We provide a highly structured workflow and domain-specific data format to improve the quality of LLM prompts. Using five RBC protocols as case studies, we have some interesting findings. First, the specification generated by TLAssist outperforms many open-source TLA$^+$ scripts we are aware of, including those written by domain experts. Second, TLAssist can assist domain experts in identifying deep design flaws. Notably, our case study on the (2,3,4)-Optimistic RBC (a CCS'25 distinguished paper) captures a subtle issue that causes the violation of the totality property. Finally, TLAssist is useful for non-experts. Namely, we show that by revising the protocols slightly, the generated error traces effectively show complex corner cases that can facilitate understanding of the design.