Writing correct distributed systems software is challenging because, in a distributed system, individual machines can fail and recover while others continue working, and because different machines execute concurrently. As a result, subtle and easy-to-miss bugs can lead to serious problems. This project’s goal is to explore the use of formal verification to develop, specify, and verify correctness of distributed systems implementations and applications.

Throughout my career at MIT I have been trying to combine my passion for math and systems, I believe that working on formally verifying complex systems is a great way to do so.