Implementing peer-to-peer systems correctly is difficult due to the extreme situations under which these systems are designed to operate. Unlike in other types of distributed systems, in peer-to-peer systems, arbitrary machines can participate in the system, and machines can leave and join the network at any time. This distinction makes it challenging to formally reason about these types of systems. In order to better understand how to design and implement certified P2P systems supporting dynamic membership, we work towards designing and verifying a peer-to-peer lookup system and a distributed hash table.

I first heard about formal verification during an internship at Oak Ridge National Lab after high school. Verification sounded really interesting, but I didn’t start learning about the subject until recently, when I took 6.888, a seminar on certified software systems. It was a ton of fun to learn about the state-of-the-art and get started on my SuperUROP project. I’m excited to work on building high-assurance systems.