In conclusion, \korg addresses a critical gap in the formal verification of distributed protocols by enabling the synthesis of communication channel-based attacks against arbitrary linear temporal logic specifications. By leveraging \spin, \korg ensures soundness and completeness in attack synthesis. Its modular support for pre-defined attacker models enhances its versatility, enabling thorough protocol analysis across diverse and interesting scenarios. We demonstrate the effectiveness of \korg by employing it to study TCP and Raft, marking it as an invaluable tool for ensuring the validity and security of distributed protocols.
