Installation

cerastes is built from source. There is no binary release. The only supported platform is macOS on Apple silicon: scripts/bootstrap.sh stops with an error on any other system.

Requirements

  • macOS on Apple silicon (arm64).

  • Homebrew.

  • The Xcode Command Line Tools (xcode-select --install). EDG parses the system C++ library and SDK headers that they provide, and the build uses their compiler.

  • A network connection on the first run. It clones the submodules, downloads the pinned Z3 release, fetches Silicon’s dependencies through sbt and installs the documentation tools from the npm registry.

  • Disk space. A bootstrapped tree takes about 5.3 GB: the third_party/ checkouts take 4.3 GB (2.8 GB of that is EDG’s own test suite), their git objects 0.3 GB, build/ 0.55 GB and doc/node_modules 0.04 GB. The Homebrew packages and the sbt caches add about 0.6 GB. Allow 7 GB.

Everything else is installed by the bootstrap script.

Build the toolchain

git clone https://github.com/cerastes-verifier/cerastes
cd cerastes
scripts/bootstrap.sh

scripts/bootstrap.sh:

  1. installs any missing prerequisite with Homebrew: CMake, Ninja, Python, ShellCheck (if they are not already on your PATH), Node (if node or npm is not on your PATH), and sbt and openjdk@17;

  2. initializes the git submodules (EDG and Silicon, which carries Silver) that are not yet checked out, and leaves a submodule that is already checked out where it is;

  3. builds EDG’s stock front end, cpfe, in build/edg;

  4. builds build/cerastes-fe, EDG’s front end in the configuration cerastes needs, with cerastes’s own back end linked in;

  5. builds build/cerastes, the verifier driver (cerastes verify);

  6. builds Silicon with sbt assembly, unless a stamp shows the jar is current;

  7. downloads Z3 4.16.0 into build/tools and checks its SHA-256;

  8. runs npm ci in doc/ to install the tools that build this documentation, unless the installed packages already match doc/package-lock.json;

  9. writes build/env.sh, which sets, among others, Z3_EXE, SILICON_JAR, CERASTES_JAVA, CPFE, CERASTES_FE and CERASTES_VERIFY for the pinned tools.

The script is idempotent: running it again changes nothing that is already current. scripts/bootstrap.sh --build-only, which scripts/check.sh uses, skips Homebrew, the Z3 download and npm ci, rebuilds what is out of date and rewrites build/env.sh. It still initializes a submodule that is missing, and rebuilds Silicon when its stamp is out of date, which can make sbt fetch dependencies. A missing or out-of-date doc/node_modules is an error that tells you to run scripts/bootstrap.sh.

In the project’s own measurement (2026-10-14), a clean clone with the Homebrew, sbt and npm caches already warm took 2 minutes 13 seconds to bootstrap and check, including building this documentation. A first run on a new machine takes longer.

The Silicon build needs JDK 17, because the sbt version Silicon pins cannot run on newer JDKs, and Silicon is tested against Z3 4.16.0. So the script uses exactly those, not whatever Homebrew has newest. To run the pinned tools by hand, load them into your shell:

. build/env.sh
"$Z3_EXE" --version

The output is Z3 version 4.16.0 - 64 bit. The versions of every pinned tool are in the toolchain pin record.

Check the installation

scripts/check.sh

This builds anything out of date, lints the scripts, checks the EDG configuration, runs the test harness’s own self-test, runs every test under tests/ and the code examples in this documentation, and finally builds this documentation. It ends with check.sh: all green when everything passes.

Try the front end

The front end parses this program, from doc/modules/ROOT/examples/installation/hello.cpp:

#include <cstdio>

int main() {
  std::printf("Hello, world!\n");
  return 0;
}

Run EDG’s stock front end on it in C++20 mode:

scripts/cpfe.sh --c++20 --no_code_gen doc/modules/ROOT/examples/installation/hello.cpp

The script finds build/env.sh itself, so you do not need to load it first. It adds the system header paths and the --clang_version that EDG needs. When the file is accepted there is no output and the exit status is 0.

--no_code_gen matters. Without it, EDG’s stock front end also writes its translation of the program to a file in the current directory (here, hello.int.c).

A syntax error is reported as an error: message that quotes the source line and marks the position, and the exit status is 2.

Verify your first program

build/cerastes verifies a source file against the contracts written in it. This function, from doc/modules/ROOT/examples/verifying/midpoint.cpp, returns a number between two others:

#include <cerastes.h>

int midpoint(int lo, int hi)
    CERASTES_REQUIRES(0 <= lo && lo <= hi)
    CERASTES_ENSURES(r, lo <= r && r <= hi)
{
  return lo + (hi - lo) / 2;
}

Verify it:

build/cerastes verify doc/modules/ROOT/examples/verifying/midpoint.cpp
doc/modules/ROOT/examples/verifying/midpoint.cpp: verified (1 function; one translation unit: assumes that functions defined elsewhere satisfy the contracts declared here)

The exit status is 0. Now verify a version with a plausible mistake, which computes the midpoint as (lo + hi) / 2:

#include <cerastes.h>

int midpoint(int lo, int hi)
    CERASTES_REQUIRES(0 <= lo && lo <= hi)
    CERASTES_ENSURES(r, lo <= r && r <= hi)
{
  return (lo + hi) / 2;
}
build/cerastes verify doc/modules/ROOT/examples/verifying/midpoint_overflow.cpp
doc/modules/ROOT/examples/verifying/midpoint_overflow.cpp:10: error: overflow: signed `int` addition may overflow

The line is the line of the source, and the exit status is 1: when lo and hi are both large, their sum does not fit in an int. The precondition allows that, so the verifier cannot exclude it. Verifying a program describes the command, and Error messages explains every category.

Build this documentation

scripts/build_docs.sh

The site is written to build/doc/; open build/doc/index.html in a browser. The build fails on any warning, such as a broken cross-reference or include. The code examples on these pages are test files, which scripts/check.sh runs.

Known limitations

  • macOS on Apple silicon only. scripts/bootstrap.sh refuses to run elsewhere.

  • Some SDK headers do not parse. With the macOS SDK 27.0 that was checked, the libc++ headers that were tried parse, among them <algorithm>, <string>, <vector>, <iostream>, <map>, <format>, <ranges> and <filesystem>. Apple’s <simd/simd.h>, and the framework headers that include it, do not: the EDG front end does not support element access on vector types (v.x). This is a limitation of the EDG front end at the pinned commit, not of cerastes itself.

  • The system headers are not pinned. EDG reads the headers of the Command Line Tools that are installed on your machine, so a different SDK version can change what parses.