IC3Syn：结合符号验证与语言模型合成分布式协议不变式

分布式协议很难被正确验证。证明安全性通常需要归纳不变式：既蕴含所需性质，又在每次协议转换后保持成立。推断这些不变式仍是主要瓶颈，现有方法常限制协议逻辑范围或依赖专家编写模板。IC3Syn 是神经符号框架，借助大语言模型，在 TLA+ 状态上执行 IC3 式过程合成归纳不变式。符号控制器将任务分解为局部阻断问题，语言模型提供单独 IC3 所欠缺的协议层推理，从而在不限制逻辑、无需手工模板的情况下组织搜索。 研究在涵盖共识、重配置和客户端—服务器系统的 29 种协议上评测，并与 Endive、IC3PO、SWISS 和 DistAI 比较。IC3Syn 为全部协议找到候选不变式，包括对照工具未报告解的工业规模 Raft 重配置协议 MongoLoglessDynamicRaft，以及一个复杂 Paxos 变体。各有限实例上合成的不变式随后在 TLAPS 中证明，对完整无界协议也具有归纳性，从而建立安全性。