Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models

Weining Cao, Guangyuan Wu, Yuan Yao +3

Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved b…