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.

Website | API Documentation

Table of Contents #

• Getting Started
  • Prerequisites
  • Building from Source
  • Installing Rust Frontends
• Using Soteria as a Library
• Soteria Rust
• Soteria-C
• Contributing
• License

Getting Started #

Prerequisites #

Before building Soteria, ensure you have the following installed:

For Soteria Rust, you will also need:

Note: Both frontends are required to run the full test suite.

Building from Source #

1. Clone the repository:

   git clone https://github.com/soteria-tools/soteria.git
   cd soteria
   

2. 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
   

3. Build the project:

   dune build
   

4. Verify the installation by running the test suite:

   dune test
   

   Note: Running dune test requires 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
   

Installing Rust Frontends #

To use Soteria Rust, you need a frontend to translate Rust code to an intermediate representation. We support two frontends:

Installing Obol #

Obol is the default frontend (recommended for most use cases).

1. Clone Obol at the correct commit:

   git clone https://github.com/soteria-tools/obol.git
   cd obol
   git checkout <COMMIT HASH> # See OBOL_COMMIT_HASH in .github/workflows/ci.yml
   

   Note: The required commit hash can always be found in .github/workflows/ci.yml under OBOL_COMMIT_HASH.

2. Build Obol:

   make build
   

3. Add Obol to your PATH:

   export PATH="$PATH:$(pwd)/bin"
   

   Add this line to your shell profile (.bashrc, .zshrc, etc.) to make it permanent.

Installing Charon #

Charon is an alternative frontend. To use it, pass --frontend charon to soteria-rust.

1. Clone Charon at the correct commit:

   git clone https://github.com/soteria-tools/charon.git
   cd charon
   git checkout <COMMIT HASH> # See charon's commit hash in soteria-rust.opam
   

   Note: The required commit hash can always be found in soteria-rust.opam under pin-depends.

2. Build Charon:

   make build-charon-rust
   

3. Add Charon to your PATH:

   export PATH="$PATH:$(pwd)/bin"
   

   Add this line to your shell profile (.bashrc, .zshrc, etc.) to make it permanent.

Using Soteria as a Library #

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 #

Soteria Rust is a Kani-like symbolic execution engine for Rust. It is in heavy development.

Usage #

Run on a standalone Rust file, symbolically executing the main function:

soteria-rust rustc <file.rs>

Run in Kani mode to execute any function with the #[kani::proof] attribute:

soteria-rust rustc --kani <file.rs>

Run all tests in a crate:

soteria-rust cargo <crate-dir>

Use --help with any command for a full list of options:

soteria-rust rustc --help
soteria-rust cargo --help

Testing Against External Suites #

To 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 miri

Limitations #

Soteria Rust supports a large subset of Rust, but some features are not yet supported:

• Concurrency
• Inline assembly
• SIMD intrinsics

Soteria-C #

Soteria-C is an automatic bug finder for C programs. It is in heavy development.

Usage #

Run on a standalone C file:

soteria-c exec-main <file.c>

Run with a compilation database:

soteria-c capture-db compile_commands.json

Use --help for a full list of options:

soteria-c --help

Contributing #

We 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

License #

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.