Soteria is a library for writing efficient symbolic interpreters directly in OCaml. The core library is just a small toolbox that we use for writing a set of analyses, currently for Rust and C.
Before using Soteria, ensure you have the following installed:
| Dependency | Version | Installation |
|---|---|---|
| OCaml | >= 5.4.0 | ocaml.org/docs/installing-ocaml |
| opam | >= 2.0 | Included with OCaml installation |
| Z3 | latest | github.com/Z3Prover/z3 |
For Soteria Rust, you will also need:
| Dependency | Version | Installation |
|---|---|---|
| Rust | nightly | rustup.rs |
| Obol | see below | Installing Obol |
| Charon | see below | Installing Charon |
Note: Both frontends are required to run the full test suite.
For users who want to install and use Soteria
-
Clone the repository:
git clone https://github.com/soteria-tools/soteria.git cd soteria -
Create a global opam switch and install:
make glob-switch && make installThis creates a global opam switch called
soteria-install, switches to it, and installs Soteria. -
Activate the switch:
eval $(opam env --switch=soteria-install)
Add this line to your shell profile (
.bashrc,.zshrc, etc.) to make it permanent, or runopam switch soteria-installto switch to it in your current shell.
For developers who want to contribute to Soteria
-
Clone the repository:
git clone https://github.com/soteria-tools/soteria.git cd soteria -
Create a local opam switch and install dependencies:
make switch
This creates an isolated OCaml environment with all required dependencies.
Alternatively, if you already have a switch you want to use:
make ocaml-deps
-
Build the project:
dune build
-
Verify the installation by running the test suite:
dune testNote: Running
dune testrequires both Rust frontends (Obol and Charon) to be installed. To run only the core Soteria or Soteria-C tests without Rust frontends:dune test soteria # Core library tests only dune test soteria-c # Soteria-C tests only
To use Soteria Rust, you need to install the supported frontends
To use Soteria Rust, you need a frontend to translate Rust code to an intermediate representation.We support two frontends: Obol and Charon.
Quick Setup: Use the versionsync script to automatically install both frontends:
./scripts/versionsync.py pull all --initThis will clone and build both Obol and Charon at the correct commits.
Obol is the default frontend (recommended for most use cases).
Using the versionsync script (recommended):
./scripts/versionsync.py pull obol --initManual installation:
-
Clone Obol at the correct commit:
cd .. git clone https://github.com/soteria-tools/obol.git cd obol git checkout 745a7e8f59596f4e656169e5b1b4f9e834c4c671
Note: The required commit hash can always be found in
scripts/versions.jsonunderOBOL_COMMIT_HASH. -
Build Obol:
make build
-
Add Obol to your PATH:
export PATH="$PATH:$(pwd)/bin"
Add this line to your shell profile (
.bashrc,.zshrc, etc.) to make it permanent.
Charon is an alternative frontend. To use it, pass --frontend charon to soteria-rust.
Using the versionsync script (recommended):
./scripts/versionsync.py pull charon --initManual installation:
-
Clone Charon at the correct commit:
cd .. git clone https://github.com/soteria-tools/charon.git cd charon git checkout 6aee301e2c0365f48f27194c50df1398f9d5647c
Note: The required commit hash can always be found in
scripts/versions.jsonunderCHARON_COMMIT_HASH. -
Build Charon:
make build-charon-rust
-
Add Charon to your PATH:
export PATH="$PATH:$(pwd)/bin"
Add this line to your shell profile (
.bashrc,.zshrc, etc.) to make it permanent.
Soteria can be used as a library to build your own symbolic execution engines. The API documentation provides a complete reference, and includes a tutorial on how to get started building your own analysis tools.
Soteria Rust is a Kani-like symbolic execution engine for Rust. It is in heavy development.
Run on a standalone Rust file, symbolically executing the main function:
soteria-rust exec <file.rs>Run in Kani mode to execute any function with the #[kani::proof] attribute:
soteria-rust exec --kani <file.rs>Run all tests in a crate:
soteria-rust exec <crate-dir>Use --help with any command for a full list of options:
soteria-rust exec --helpTo test Soteria Rust against external test suites:
# Test against the Kani test suite
git clone https://github.com/model-checking/kani.git ../kani
soteria-rust/scripts/test.py kani
# Test against the Miri test suite
git clone https://github.com/rust-lang/miri.git ../miri
soteria-rust/scripts/test.py miriSoteria Rust supports a large subset of Rust, but some features are not yet supported:
- Concurrency
- Inline assembly
- SIMD intrinsics
Soteria-C is an automatic bug finder for C programs. It is in heavy development.
Run on a standalone C file:
soteria-c exec-main <file.c>Run with a compilation database:
soteria-c capture-db compile_commands.jsonUse --help for a full list of options:
soteria-c --helpWe welcome contributions from the community! Soteria is open source and will remain open source.
Soteria is developed and maintained by Soteria Tools Ltd. The core team makes final decisions on project direction, but we value community input and aim to be transparent about our decision-making process.
- Chat with us: Join our Zulip chat to ask questions or discuss ideas
- Submit a PR: Read our contribution guidelines first
- License agreement: Review the Contributor License Agreement before contributing
Soteria and derived tools in this repository are under Apache-2.0 license, copyright Soteria Tools Ltd 2026.
The Soteria logo is a trademark of the Soteria Tools Ltd.