Brent Spell on GoJournal: a verified, concurrent, crash-safe journaling system
Details
Link: https://www.chajed.io/papers/gojournal:osdi2021.pdf
Description: GoJournal is a concurrent journaling system written in Go; aiming to close the gap between formal verification and implementation, they use Perennial 2.0 which aims to provide tools for modular proofs and crash-safety guarantees. The modularity is used to formally verify not just the abstract protocol but also the internal APIs of GoJournal.
Bio: Brent is the chief technology officer of Spokestack. When he isn't working on machine learning systems for speech, he can be found reading papers, building prototypes, and curating the best memes the internet has to offer.