Parallel & Distributed Operating Systems Group

Armada: verifying concurrent storage systems

Project overview

Armada 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 Armada.

Armada 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.

People