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.
- Tej Chajed (PhD)
- Joe Tassarotti (postdoc)
- Prof. M. Frans Kaashoek
- Prof. Nickolai Zeldovich