Soteria is an OCaml library for writing efficient symbolic interpreters directly in OCaml.
The core library provides a set of batteries-included abstractions for writing one's own symbolic interpreter. Currently, two symbolic interpreters have been written: Soteria Rust and Soteria C. Our current main focus is Soteria Rust.
Table of Contents
Getting Started
Install Soteria Rust
For users wishing to user Soteria Rust for writing and running symbolic tests, we strongly recommend installing Soteria Rust through cargo on macOS with M-series chips and Linux x86_64:
cargo install soteria
cargo soteria setup # Installs pre-built binaries
# setup can be run again at every nightly release of Soteria Rust (every day).
For other architectures, please follow the manual installation instructions in the contributing guide.
Install the Soteria Library
Soteria can be used as an OCaml 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.
Pin it with opam:
opam pin add soteria git+https://github.com/soteria-tools/soteria.git#<commit>
Soteria Rust
Soteria Rust is a symbolic execution engine for Rust. It is in heavy development.
Usage when installed from cargo
Using cargo soteria, the tests inside of the current crate can be run using:
cargo soteria
If the crate contains Kani harnesses, the Kani compatibility layer can be enabled with:
cargo soteria --kani
The full help for cargo soteria can be obtained with:
cargo soteria --help
Usage when installed from source
Installing from source install a soteria-rust binary, which can be used as follows.
Run on a standalone Rust file, symbolically executing the main function, or any function with the #[soteria::test] attribute:
soteria-rust exec <file.rs>
Run all tests in a crate:
soteria-rust exec <crate-dir>
Run in Kani mode to execute any function with the #[kani::proof] attribute, with compatibility with the Kani api (e.g. kani::any):
soteria-rust exec --kani <file.rs>
Use --help with any command for a full list of options:
soteria-rust exec --help
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.
Installatation
Binaries for Linux x86 and MacOS Arm are available in the latest release on this GitHub repository. For other architectures, please follow the manual installation instructions.
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.
AI Policy
We welcome contributions assisted by AI, as long as they follow our AI Policy.
Acknowledgements
Soteria relies on many excellent open source libraries and tools, and we are deeply grateful to their authors and contributors.
We would especially like to thank:
- The Charon team for providing the MIR frontend that powers Soteria Rust
- The Cerberus team for providing the C frontend that powers Soteria C
License
Soteria and derived tools in this repository are under the Apache-2.0 license, see LICENSE. Copyright 2024–2025 Imperial College London and 2025–2026 Soteria Tools Ltd.; see the NOTICE file for how copyright is split between the two.
Third-party components linked into or shipped with the Soteria binaries are listed in THIRD_PARTY_NOTICES, with their license texts in third-party-licenses/.
The Soteria logo is a trademark of the Soteria Tools Ltd.
