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.

Website | API Documentation

Table of Contents #

• Getting Started
• Soteria Rust
• Soteria C
• Contributing
• Acknowledgements
• License

Getting Started #

Install the Soteria 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.

Pin it with opam:

opam pin add soteria git+https://github.com/soteria-tools/soteria.git#<commit>

Install Soteria Rust #

Soteria Rust can be installed with cargo on macOS with M-series chips and Linux x86_64:

cargo install soteria --git https://github.com/soteria-tools/cargo-soteria.git

For other architectures, please follow the manual installation instructions in the contributing guide.

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

• 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

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 Apache-2.0 license, copyright Soteria Tools Ltd 2026.

The Soteria logo is a trademark of the Soteria Tools Ltd.