Introducing Soteria: A New Generation of Static Analysis for Rust - Soteria
Back to Blog Introducing Soteria: A New Generation of Static Analysis for Rust<br>Find bugs today. Teach AI to find them tomorrow.
Azalea Raad · 10 June 2026<br>RSS<br>Software engineering is changing faster than ever.<br>AI coding assistants can generate thousands of lines of code in seconds. Large language models are becoming part of everyday development workflows. Codebases are growing larger, more complex, and increasingly distributed across teams and services. But one thing hasn’t changed:<br>Bugs are still expensive!<br>…and in the age of AI-generated code, they may become even more so. Today, we’re excited to introduce Soteria : a new static analysis platform designed to find real bugs in Rust and C codebases with unprecedented precision, speed and semantic accuracy.<br>We are academics specialised in program analysis and automated reasoning tools, and we’ve spent years building static analysis tools for industry. We’ve seen firsthand how powerful these tools can be, but also how difficult they are to build and maintain. Soteria is the culmination of that experience, and represents a new vision for what static analysis can be in the age of AI.<br>Beyond that, Soteria is built for the future of software engineering: a future where humans and AI write code together, and where automated reasoning about programs becomes as essential as testing and CI.<br>Why Static Analysis Matters More Than Ever
The rise of AI-assisted programming is transforming how software gets written.<br>Developers are no longer typing every line manually. Instead, they increasingly review, adapt, and integrate code generated by AI systems. This shift dramatically increases productivity, but it also creates a new challenge.<br>AI-generated code can look convincing while containing subtle bugs: memory safety violations, integer overflows, incorrect assumptions about aliasing, missing edge cases, violations that may only emerge under rare execution paths, and so forth.<br>Traditional testing helps, but testing can only check the paths you explicitly execute. Static analysis approaches the problem differently.<br>Instead of asking:<br>“Does this program work for the inputs I tested?”
Static analysis asks:<br>“What could happen for all possible inputs?”
That difference is enormous!<br>A powerful static analysis engine can discover bugs before they’re deployed. In a world where AI can generate code at scale, automated reasoning about code becomes a necessity, not a luxury.<br>The Rust Revolution
At the same time, another major shift is underway. The software industry is steadily moving toward Rust. Organisations including Microsoft, Google, Amazon Web Services and Meta have all invested heavily in Rust adoption because of its unique combination of performance comparable to C and C++, strong memory safety guarantees, modern tooling and developer experience, and reduced vulnerability rates in critical systems.<br>Rust has already become one of the most influential systems programming languages of the last decade. Yet despite Rust’s impressive safety guarantees, there remains a widespread misconception:<br>“Rust is memory-safe, so analysis tools aren’t necessary.”
The reality is more nuanced. Rust eliminates entire classes of bugs, but developers can still write incorrect code. Rust is not a silver bullet: its safety guarantees (ensured by its type system) are compromised by writing unsafe Rust code that bypasses the Rust type system. It is inevitable that developers end up resorting to unsafe when they need to express abstractions that are too low-level for the type system.<br>Additionally, logical bugs (about the functional correctness of the code), arithmetic issues, concurrency problems and subtle semantic violations can occur even in safe Rust code!<br>As Rust adoption accelerates across industry, the need for advanced analysis tools becomes increasingly important.<br>That’s where Soteria comes in!<br>Meet Soteria
Soteria is a static analysis platform powered by symbolic execution .<br>Rather than executing your code with a single input, symbolic execution explores all possible execution paths simultaneously. Think of it as a systematic search through the behaviour of your program.<br>Instead of checking:<br>foo(42)
Soteria effectively asks:<br>foo(any_possible_input)
…and reasons about what could happen.<br>This allows Soteria to uncover bugs that traditional testing cannot detect, such as memory safety and aliasing violations, invalid pointer usage, and other types of undefined behaviour (UB).<br>The result is deeper coverage, stronger guarantees and more confidence in your software.<br>Symbolic execution will branch at any decision point in your program and explore each branch until the program terminates or an error or UB is reached. This technique has a long history in research, and has been battle-tested by industry. Try the demo below to see how Soteria would explore a simple piece of code.<br>1 if x 0 {<br>2 x = -x;<br>3 }<br>4 assert!(x >=...