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 C and Rust.

Build instructions #

To build the current repository, you first need to install OCaml. We then advise to create a local switch for development, and build the project:

opam switch create . --deps-only -y
dune build @all

If you want to run the build version of the code, you must also install Z3.

You can make sure that everything is working properly by running the test suite:

dune test

Soteria-c (working name) #

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

It can currently be tested on standalone files by opening this project in VSCode. To do so, open the Run and Debug tab of the sidebar, select the "Launch (Local)" configuration and click the "play" button.

Rusteria (soteria-rust) #

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

It can run standalone files, symbolically executing the main function, or any function with the attribute #[kani::proof], if in Kani mode (--kani).

soteria-rust rustc <file>

It can also run all tests in a crate:

soteria-rust cargo <crate dir>

You may add --help to either of these commands to see all available options.

Frontend #

To use Rusteria you must have a frontend installed; we support Obol (recommended) and Charon.

To use Obol, you must add the --obol flag to soteria-rust commands, and have the obol command on your path. To do so:

clone Obol
run make build
add obol/bin to your path (e.g. export PATH=$PATH:/path/to/obol/bin)

To use Charon, you must have the charon command on your path. To do so:

clone Charon
run make build-charon-rust
add charon/bin to your path (e.g. export PATH=$PATH:/path/to/charon/bin)

Testing #

To test Rusteria on the Kani test suite, clone Kani next to soteria, and run soteria-rust/scripts/test.py kani.

You can also test Rusteria on the Miri test suite: clone Miri next to soteria and run soteria-rust/scripts/test.py miri.

Limitations #

Soteria-rust supports a large subset of Rust, but is still in development. Some currently unsupported features include:

Concurrency
Inline assembly
SIMD intrinsics
Trait objects (dyn Trait)

Currently, and unlike Soteria-C, Soteria-Rust has neither IDE integration or compositionality support (all tests must instead start from an entry point). We are actively working on the latter!

License #

Soteria and derived tools in this repository are under Apache-2.0 license, copyright Soteria Team 2025.

The Soteria logo is a trademark of the Soteria Team.

Clone this repository