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:
- Low-level: You can verify programs that, for performance reasons or otherwise, can't tolerate any abstraction beyond that associated with assembly language.
- Foundational: The output of a Bedrock verification is a theorem whose statement depends only on the predicates you choose to use in the key specifications and on the operational semantics of a simple cross-platform machine language. That is, you don't need to trust that the verification framework is bug-free; rather, you need to trust the usual Coq proof-checker and the formalization of the machine language semantics.
- Higher-order: Bedrock facilitates quite pleasant reasoning about code pointers as data.
- Computational: Many useful functions are specified most effectively by comparing with "reference implementations" in a pure functional language. Bedrock supports that model, backed by the full expressive power of Coq's usual programming language.
- Structured: Bedrock is an extensible programming language: any client program may add new control flow constructs by providing their proof rules. For example, adding high-level syntax for your own calling convention or exception handling construct is relatively straightforward and does not require tweaking the core library code.
- Mostly automated: Tactics automate verification condition generation (in a form inspired by separation logic) and most of the process of discharging those conditions. Many interesting programs can be verified with zero manual proof effort, in stark contrast to most Coq developments.
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