Mike He is a Princeton PhD student working at the intersection of formal verification and distributed systems. He will be presenting Specy : Learning Specifications for Distributed Systems from Event Traces, an OOPSLA '26 paper!

We will be meeting Monday, April 13th, from 6:30 to 7:30 PM in CoC 053, and hope to see you there! If you can't make it in person, a zoom link is also provided.

For any additional information, please don't hesitate to reach out via our discord: https://discord.gg/cyNvsmtjqY

Below is an abstract of the work:
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.