coq-vsu

Tools for working with Verified Software Units.

Note

This is a work in progress! We welcome feedback and pull requests. Find us on GitHub.

What is a Verified Software Unit?

A verified software unit (VSU) is a C library that has been proven correct using the Verified Software Toolchain.

The theory of VSUs was introduced by Verified Software Units (Beringer, 2021). Examples of how to use VST to build VSUs are given in Software Foundations Volume 5: Verifiable C.

What is coq-vsu?

A typical VSU consists of a library written in Coq that proves functional correctness of a library written in C.

This unique project structure is not natively supported by opam. In particular, opam provides no guidance on questions such as Where should the C library be installed to? and How will users configure their compiler to find it?

coq-vsu answers these questions with a single tool: vsu, which has the magic ability to locate paths.

For a simple example of coq-vsu in action, see coq-vsu-int63.