Documentation
Everything you need to get started with and integrate powerful bug detection into your workflow.
Soteria Rust
Learn how to use Soteria Rust for symbolic execution of Rust codebases
Soteria C
Explore the full capabilities of our compositional C analysis tool
Library Documentation
Read through the documentation of the Soteria library
Source Code
Browse the source on GitHub
FAQ
Common questions about Soteria answered
Roadmap
See what's coming next for Soteria
Soteria is a library for writing efficient symbolic interpreters directly in OCaml. The core library is a powerful toolbox used for building a set of analyses, currently targeting Rust and C.
Soteria uses symbolic execution to find bugs that traditional testing might miss. Instead of running your code with concrete values, Soteria explores multiple execution paths simultaneously, uncovering edge cases and potential vulnerabilities.
Soteria Rust
A Kani-like symbolic execution engine for Rust. It can run standalone files or entire crates, symbolically executing main functions or Kani proof harnesses.
Soteria C
A symbolic execution tool for C programs. Currently in heavy development, it can detect memory errors, null pointer dereferences, and more.
Fuller instructions available on the Getting Started page.
Install OCaml
First, you'll need to install OCaml on your system.
Clone and Build
Create a local switch and build the project: make switch
Install Z3
To run the built version, you must also install Z3 .
Run Tests
Verify everything works properly: dune test
Soteria Rust - Single File
soteria-rust exec <file>Symbolically execute a single Rust file
Soteria Rust - Crate
soteria-rust exec <crate-dir>Run all tests in a crate
Soteria C bi-abduction
soteria-c exec file1.c file2.c -I .Analyse all functions across a list of files
Add --help to any command to see all available options, or visit the
documentation of each tool for more detailed guides.