FMitF: Track 1: Pay-as-you-go Consistency Verification for Distributed System Designs

Distributed systems are foundational in modern computing infrastructure. Applications built on top of a distributed system rely upon the system's consistency model to provide guarantees about how the system and the application may interact. If a system fails to provide its stated consistency model, the correctness of any application built on top of it is in jeopardy. Previous work has demonstrated that it is possible to build real systems that provably provide consistency guarantees. However, the burden of formally proving consistency is extremely high, and so formal methods are not widely used by distributed system designers. The objective of this project is to smooth the effort-to-value curve of formal methods tools. This project develops technology for both refuting and proving consistency properties of distributed system designs. The goal is to provide a pay-as-you-go workflow for creating correct system designs, wherein the designer may put in incrementally more effort into the verification process to gain proportionally more confidence in the correctness of their design. The technology will be implemented in open-source software, freely-available to distributed systems designers, with the ultimate goal of increasing the adoption of formal methods and enabling the creation of more reliable systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.