Principal Investigator Adam Chlipala
Project Website http://adam.chlipala.net/bedrock/
Bedrock, a new low-level programming language, embedded within Coq, with support for mostly-automated verification of functional correctness. My goal is to use Bedrock to implement a complete verified software stack that can rely on static verification to take over from uses of dynamic techniques for enforcing process isolation.
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 some 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. For instance, the examples in the distribution include a function memoizer and a cooperative threads library, each involving less than a page of (very high-level) proofs.
(*) 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. Manual proof effort is generally confined to, first, annotations specifying which simplification rules for abstract impure predicates should be applied at which program points; and, second, hint lemmas about mathematical objects like sets, maps, and lists.