coq-vsu-int63

Published by applied.fm.

A Verified Software Unit for 63-bit integer arithmetic.

Implemented in C, modeled in Coq, and proven correct using the Verified Software Toolchain.

Compatible with CompCert.

Note

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

C library

See our Doxygen docs.

Coq library

• Coq model

• Coq specs

• Coq proofs