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 l