Project Description

Distributed storage systems form the backbone of modern internet services. However, maintaining correctness and extracting good performance while ensuring resilience to real-world disruptions like server failures, network faults, and clock drifts, remains challenging. Therefore, the cloud industry has adopted various verification tools like model checkers, fault injection frameworks, and proof checkers to test and verify their protocols and implementations.

In this project, we aim to improve upon the existing verification foundation. Some ideas include scaling up verification tools by improving core algorithms, generalizing them to include new types of failures like gray failures and metastable failures, and using LLM-based proof agents to reduce the verification burden.