CSE researchers win Best Paper Award at OSDI 2025

July 10, 2025
They were recognized for their development of Basilisk, an automated approach for formally verifying distributed protocols.

CSE researchers received a Best Paper Award at the 2025 USENIX Symposium on Operating Systems Design and Implementation (OSDI) for their paper titled “Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols.” The team was recognized for their novel contributions to automated formal verification, substantially improving the safety and reliability of distributed systems.

OSDI is a premier conference for operating systems research, bringing together leaders from academia and industry to explore the design, implementation, and analysis of modern systems software. The Best Paper Award is given each year to research that exemplifies significant, original, and impactful advances in the field. Two winning papers were selected from 53 total accepted submissions for this honor.

The research was led by first author Tony Zhang, a recent CSE PhD grad, and coauthored by Prof. Manos Kapritsos and CSE alum Keshav Singh. Other authors on the paper include Tej Chajed of the University of Wisconsin–Madison and Bryan Parno of Carnegie Mellon University.

The paper introduces Basilisk, a new tool that automates the process of safety assurance for distributed protocols, systems that allow computers to reliably coordinate over networks. Formal verification has become a critical method to ensure the safety of these protocols, but this process hinges on finding complex inductive invariants, precise properties that must hold in the initial state and after every possible step, proving a system will always remain safe. This task is highly labor-intensive, sometimes taking experts weeks or even months for a single protocol. 

Diagram showing the Basilisk workflow for protocol verification. Four sequential steps are illustrated: (1) the user defines a protocol; (2) Basilisk generates a history-preserving asynchronous protocol; (3) Basilisk generates an inductive invariant and its inductiveness proof; and (4) the user proves the invariant implies a safety property. A dashed feedback loop from step 4 to 3 allows user hints to refine weak invariants.
Basilisk workflow. Shaded bubbles represent artifacts that the user writes, while white boxes represent artifacts that Basilisk generates. In a few cases, the user may discover while writing the proof in step 4 that the inductive invariant I generated in step 3 is too weak. In such cases, the user provides hints (the dashed arrow) that enable Basilisk to generate a stronger invariant.

Basilisk addresses this challenge with two techniques. First, rather than searching for complex invariants across multiple hosts, it is able to establish safety properties by piecing together many simpler Provenance Invariants, which track the lineage of hosts’ states throughout the system’s execution. Second, Basilisk uses a new technique called atomic sharding to automatically identify Provenance Invariants. By combining these two approaches, Basilisk automatically generates and proves the required inductive invariants for a wide variety of distributed protocols.

The authors applied Basilisk to 16 challenging distributed protocols, demonstrating that it can automatically synthesize inductive invariants with little or no developer input. This approach paves the way for more reliable and robust distributed systems, minimizing manual errors while significantly advancing the usability of formal verification in systems research.

By enabling practical, automatic verification of complex distributed protocols, this research has major implications for the reliability and trustworthiness of the systems that underpin modern computing.