Crucible turns imperative programs into control-flow graphs and searches them symbolically

Forward symbolic execution over control-flow graphs

Crucible is described in the README as a language-agnostic library for performing forward symbolic execution of imperative programs. Two words in that sentence carry the design.

Forward means the engine walks a program from its entry point along a path, maintaining a symbolic state rather than concrete values. Language-agnostic means the simulator core knows nothing about any particular source language. Instead, the README says it provides a collection of data-structures and APIs for expressing programs as control-flow graphs, and that programs expressed as CFGs in this way can be automatically explored by the symbolic execution engine.

So the contribution model is inverted from what you might expect. Rather than writing a front end that teaches a symbolic engine about a language, you build a CFG for the program and hand it over. The cost of that choice is that you must supply the semantics yourself: what a memory read means, what a call does, what a particular instruction does to the state.

That is why the project is structured as a set of packages rather than one program. Crucible core gives you the simulator and the CFG representation, and everything language specific lives in a front end that translates source or bytecode into those CFGs and then implements the primitives the simulator needs.

What4 carries the formulas and talks to the solvers

The engine needs a way to represent conditions that are not yet decided, and a way to ask whether a set of those conditions is satisfiable. Crucible delegates that to another library. The README states that Crucible relies on an underlying library called What4 that provides formula representations and connections to a variety of SAT and SMT solvers, used to perform verification and to find counterexamples to logical conditions computed from program simulation.

The division of labour is clean. Crucible builds a symbolic state and accumulates path conditions as it explores. What4 owns the formula language, the theory combination, and the solver interface. When the engine wants to know whether a branch is feasible, or whether an assertion can be violated, that question goes down to What4 and comes back as a model, and the model is the counterexample.

Crucible also allows the model to be extended from outside. The README notes that new data types and operations can be added to the symbolic simulator by implementing fresh primitives directly in Haskell. That is the extension point that makes the library interesting for language work: if you are building a front end for a language with an unusual memory model, you implement its primitives against Crucible's interfaces rather than forking the engine.

The dependency surface is kept small on purpose. The README says Crucible has been designed as a set of Haskell packages organized so that Crucible itself has a minimal number of external dependencies, and that functionality independent of crucible can be separated into sub-libraries.

Front ends for LLVM, the JVM, Rust and beyond

The repository is a Haskell package collection, and the front ends are the most visible part of it. The README lists crucible-llvm, which provides translation and runtime support for executing LLVM assembly programs in the Crucible symbolic simulator, and crucible-jvm, which does the same for JVM bytecode programs.

The tree at the repository root shows the full spread, and it is wider than the README's summary. Alongside crucible/, crucible-llvm/, crucible-jvm/ and the CLI and syntax packages, the top level contains crucible-concurrency/, crucible-go/, crucible-symio/, crucible-wasm/, and a crux-test-gen/ directory, plus a dependencies/ directory, a doc/ directory and a scripts/ directory.

The names hint at the scope: a concurrency frontend, a Go frontend, a WASM frontend, and a package for generating tests. The README does not describe these in detail, so treat them as separate efforts with their own documentation rather than as one unified feature set.

Each front end pairs a translation step with a runtime support layer. crux-llvm, for instance, is a standalone frontend for executing C and C++ programs in the crucible symbolic simulator, and it invokes clang to produce LLVM bitcode before running the result with the crucible-llvm language frontend. The LLVM approach means the semantics are attached to a bitcode-level model rather than to a C-level one, which is why clang is a prerequisite rather than an optional extra.

Building the workspace with cabal and pinned dependency versions

Crucible is built from a clone of the repository, and the README's quick start is short. It asks you to check out the immediate submodules to supply the needed dependencies, then build with the cabal tool.

git submodule update --init

cabal update
cabal new-configure
cabal new-build all

The README notes that you can target a more specific sub-package instead of all, which matters because a full build of every front end is a large compile. Tests run through cabal test, and coverage is enabled with cabal test --enable-coverage or cabal configure --enable-coverage, with the README warning that extra workarounds are needed for the coverage build.

The version pinning deserves attention. The repository ships cabal.GHC-9.8.4.config, cabal.GHC-9.10.3.config and cabal.GHC-9.12.2.config, files that constrain dependency versions in CI, and the README recommends linking the one matching your compiler to cabal.project.freeze before building locally, so your local build resolves the same versions as CI.

Those files were generated with cabal freeze --enable-tests --enable-benchmarks. The README also states that they assume a Unix-like operating system, because Windows is not tested in CI, and lists the packages to remove by hand if you are on Windows: regex-posix, tasty +unix, unix, unix-compat.

Testing crux-mir has extra prerequisites: the mir-json tool must be built and installed and reachable on your $PATH, and you need translated Rust libraries for the machine you are testing on.

Two ways to run a program: the crux wrapper or the interactive debugger

Crucible offers two distinct approaches to putting a program under the engine, and choosing between them is a real decision rather than a preference.

The first is the crux package, which the README describes as common support libraries for running the crucible simulator in a basic all-at-once use mode for simulation and verification. It includes most of the setup steps required to actually set the simulator off and running, along with functionality for collecting and discharging safety conditions and generated assertions via solvers. Both the crux-llvm and crucible-jvm executables are thin wrappers around this functionality.

The second is the interactive route. crucible-debug provides an interactive debugger for Crucible programs, and the crucible-cli, crucible-llvm-cli, crucible-mir-cli and crucible-llvm-debug packages extend the same idea to specific languages and memory models. Programs for these tools are written in crucible-syntax, a native S-Expression based concrete syntax for Crucible programs.

The difference in practice is where the loop closes. The all-at-once mode is batch: you give it a program, it explores, and it reports conditions it could or could not discharge. The debugger and CLI route is where a human sits inside the exploration, which the README motivates by making it possible to interact with the core simulator directly without bringing in the issues of another front end, such as the LLVM translation.

There is also a third entry point for benchmarking. crux-llvm-svcomp is an alternative entrypoint to crux-llvm that uses the protocol established for the SV-COMP competition, so a Crucible based setup can be measured against other verification systems on the same tasks.

Rust support arrives through the crux-mir backend

Rust is handled in a way that is worth understanding before you try it, because it is not the same shape as the LLVM and JVM front ends.

The README describes crux-mir as a tool for executing Rust programs in the crucible symbolic simulator, and identifies it as the backend for the cargo crux-test command provided by mir-json. The pointer to mir-json is the important part: the Rust path runs through the MIR intermediate representation, and mir-json is what produces the program representation that the backend consumes.

That has a practical consequence for setup. The README states that to run the tests for crux-mir you need to have built and installed the mir-json tool such that it can be found on your $PATH, and you also need translated Rust libraries for the machine you are testing on. The latter requirement means the Rust flow is machine specific, since the translations are built for a particular target.

The Rust story is also newer than the rest of the project in the repository listing: crucible-mir/, crucible-mir-cli/, crucible-mir-debug/ and crucible-mir-syntax/ sit alongside the older crucible-llvm family, and there is a separate crux-mir README referenced for details, which is where the specifics live.

Compared with the LLVM path, where clang produces bitcode directly, the Rust path depends on an external toolchain component being installed separately. That is a real difference in setup effort between the two front ends.

PVP versioning, 0.x majors, and a busy main branch

Crucible is a research project with a specific release discipline, and knowing it saves surprises.

The README states that all library components conform to the Haskell Package Versioning Policy, and that every executable has a corresponding library and they share a version number. The consequence for users is the usual PVP one: under the PVP, a change to the API requires bumping the major version, so a cabal constraint that permits major version bumps can break your build.

There is one project-specific rule on top of that. The README says crux-llvm and crux-mir share the same version number, and that the major version of these packages is bumped on every release, regardless of the changes, or lack of changes, in each. In other words, the major number of these front ends carries no compatibility meaning. Treat them as always moving.

The repository also uses development versions, where immediately after a release a fifth version component starting at.99 is added and incremented occasionally. Downstream packages can then depend on a development version while still distinguishing it from a release.

On activity, the last push was on 2026-10-19, and the release tags show crux-v0.12 on 2026-01-29, crux-v0.11 on 2025-11-10 and crux-v0.10 on 2025-03-24. Major features are developed in separate branches based off master and merged back when complete, while minor features and bug fixes land on master directly.

Each library is BSD licensed, with a LICENSE file in each project directory, so there is no licensing obstacle to building on the packages.

Editorial conclusion

Crucible fits research and tool-building work where you need to explore a program's paths symbolically, build custom primitives for a language or memory model that no existing engine understands, or plug verification into a competition harness such as SV-COMP. It is the wrong tool for a one-off bug hunt in a normal application, for a team that does not want to maintain Haskell build dependencies, or for a project whose verification needs are met by a property-based testing library with a far smaller setup cost. Verify first that the front end matching your language exists in the repository, that a suitable What4 backend is reachable for the SAT and SMT solvers you intend to use, and that the freeze file shipped for your compiler version covers the packages you need, because those files assume a Unix-like system and Windows is not tested in CI.

Frequently asked questions

Official sources

1. GaloisInc/crucible on GitHub
2. Issues
3. License: BSD-3-Clause
4. README
5. Releases