一句话：提出 Specy，从分布式系统事件轨迹中自动学习带事件量词的规约，并支持不变式推导与运行时监控。
分布式系统的正确性推理极具挑战，而精确的规约是验证的前提；然而开发者难以识别和形式化关键规约。Specy 通过从消息交换产生的可观测事件轨迹中自动学习规约来解决这一问题。它设计了面向事件规约的专用文法，支持事件量词以刻画分布式协议中的复杂行为模式；其学习过程结合了基于文法的枚举搜索与从事件轨迹中的动态学习，有效控制规约搜索空间。在经典分布式协议和工业案例上的评估表明，Specy 能成功学到重要协议规约，发现开发者遗漏的未知规约，自动导出原本需手工构造的归纳不变式，并通过生产系统的运行时监控揭示测试覆盖缺口。
Reasoning about the correctness of distributed systems is a significant challenge, with precise correctness specifications serving as an essential prerequisite to verification. However, identifying and formulating specifications remains a major hurdle for developers in practice. Specy addresses this challenge by automatically learning specifications from observable event traces generated by message exchanges in distributed systems. The system employs a specialized grammar tailored for event-based specifications, incorporating support for quantifiers over events - a capability essential for capturing the complex behavioral patterns inherent in distributed protocols. Specy utilizes a novel learning procedure that combines grammar-based enumerative search with dynamic learning from event traces, providing effective control over the specification search. We evaluated Specy on established distributed protocols and industrial case studies, demonstrating its ability to successfully learn important protocol specifications. Specy can discover previously unidentified specifications overlooked by developers, automatically derive inductive invariants that were previously constructed manually for verification purposes, and, through run-time monitoring in production systems, reveal gaps in testing coverage - highlighting opportunities to leverage specifications in practice.
@article{paperbot3789,
title = {Specy: Learning Specifications for Distributed Systems from Event Traces},
author = {Mike He and Ankush Desai and Aishwarya Jagarapu and Doug Terry and Sharad Malik and Aarti Gupta},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798209}
}