4 papers
Argus: A General-Purpose Agentic Reasoning Runtime for Long-Horizon Tasks
Boxiu Li, Zimo Wen, Yijia Fan +24
Long-horizon reasoning requires an agentic runtime that can persist when evidence supports its current approach and pivot when measurements reveal failure, hidden constraints, or a…
Specula: Scaling formal specifications for autonomous model checking of system code
Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang +6
Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model chec…
SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
Qian Cheng, Ruize Tang, Emilie Ma +7
Formal models are essential to specifying large, complex computer systems and verifying their correctness, but are notoriously expensive to write and maintain. Recent advances in g…
Multi-Grained Specifications for Distributed System Model Checking and Verification
Lingzhi Ouyang, Xudong Sun, Ruize Tang +4
This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model fine-grained…