Bedrock, a Coq library for verified low-level programming

Bedrock is a library that turns Coq into a tool much like classical verification systems (e.g., ESC, Boogie), but niftier. In particular, Bedrock is:

Tutorial

Project Members

Code Releases (BSD license)

Our code releases tend to be quite specific to exact Coq versions, so don't expect any of the below to work in any Coq version beside the one specified; yes, even newer versions that are only off by a few characters!

Release Coq version Description
20140722 8.4pl2 Verified Web services processing XML and maintaining an in-memory relational database; a verified compiler for a C-style language
20130328 8.4 Some experiments with a thread library and some Internet servers
20121112 8.4 Fancier examples of certified macros; some automation performance tuning
20120825 8.4 Port to new Coq release; more automation for Memoize example
20120724 8.4beta2 Some small optimizations
20120710 8.4beta2 Largely a from-scratch reimplementation, where a key addition is verified proof procedures for separation logic using proof by reflection
20110712 8.3pl2 Some more experiments with Bedrock as an extensible programming language
20101027 8.2pl2 First release, associated with PLDI'11 paper

For More Information...

Project Partially Supported By

Project Alumni