Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning

We introduce a runtime-monitoring–driven framework for automatically discovering inductive invariants in distributed systems. By collecting lightweight execution traces and iteratively synthesizing classifiers that separate observed states from speculative unreachable states, our method produces invariants that are both precise and probabilistically sound. Experimental results on a suite of distributed protocols show that the approach scales to large state spaces and uncovers tight invariants that elude traditional template-based learners.

In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2025)