package soteria

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
• Soteria Rust
• Soteria C
• Contributing
• Acknowledgements
• License

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.

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