Project overview

Perennial is a Coq framework for verifying concurrent storage systems. It supports verifying systems written in Go by translating them to Coq to complete the proof using Perennial.

Perennial extends Iris, a logic for concurrent verification, with support for proving crash safety. We used Goose to write a concurrent mail server with a proof that delivered messages are never lost. We’re now using Perennial to verify a concurrent file system.