Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time
The BEDROCK Coq library
Mostly automated verification of higher-order programs with higher-order separation logic, with a small trusted code base

This release requires Coq 8.4pl2.

To build, run one of the following:
   make native
   make ltac
to select whether to use the OCaml or Ltac reification code, respectively.
By default, you get the Ltac version, which is _much_ slower (i.e., adds hours to the time to build the library and all examples serially), but avoids the need to load a plugin into Coq, which can be tricky to do on some platforms.

Then, just run (one of the two):
and go take a break while it runs for an hour or so (if you're lucky enough to have a new-ish machine). ;)  Using the '-j' switch for parallel build is highly recommended.

(2) Or:
   make cito
(no need to run "make" beforehand) to make the Cito compiler.

To make executable Cito example programs, see 'Bedrock/Platform/Cito/README'.
Also see the 'Examples', 'Platform', 'Platform/Cito', and 'Platform/Facade'
subdirectories of 'Bedrock/', and their READMEs.