Agora：利用 LLM 代理实现生产级共识协议中的自主错误检测

共识协议构成了分布式系统和区块链的支柱，其中实施错误可能会导致数据损坏和财务损失。虽然基于 LLM 的方法在代码分析方面显示出前景，但它们与涉及跨多个执行阶段的复杂状态相关行为的深层协议级逻辑错误作斗争。我们推出了 Agora，这是一个领域感知多代理框架，它将假设驱动测试与 LLM 功能集成在一起，以进行系统协议验证。 Agora 采用专门的代理来协作探索协议状态空间，使用特定领域的约束综合攻击场景，并通过迭代细化验证结果。这种显式的角色分离使得能够对单函数代码分析之外的全局协议不变量进行推理。我们使用四种最先进的 LLM 在四种共识实现（Raft、EPaxos、HotStuff、BullShark）上评估 Agora。 Agora 发现了 15 个先前未知的违反安全属性的协议级逻辑错误，而现有的基于 LLM 的代理无法检测到任何此类协议级逻辑错误。我们的结果表明，领域感知多代理协作对于检测复杂协议中的深层逻辑错误至关重要。