Sound static analysis for the masses.
Soteria uses symbolic execution to reliably find memory bugs, overflows, data races, and undefined behaviour in Rust and C codebases — at speeds that fit real development workflows.
Soteria is a static analysis tool built on symbolic execution. It exhaustively explores execution paths in your code to surface bugs that fuzzing and traditional static analysis may miss — with no false positives by design.
- 86.9% pass rate across Kani & Miri test suites
- 15.8× faster than CBMC
- 19 pp boost in LLM violation detection
soteria: The core symbolic execution engine, supporting Rust (soteria-rust) and C (soteria-c).cargo-soteria: Cargo integration for Rust projects, enabling seamless analysis withcargo soteria.