Introducing Soteria: A New Generation of Static Analysis for Rust - Soteria

Software engineering is changing faster than ever.

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:

Bugs are still expensive!

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

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.

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.

The rise of AI-assisted programming is transforming how software gets written.

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.

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.

Traditional testing helps, but testing can only check the paths you explicitly execute. Static analysis approaches the problem differently.

Instead of asking:

“Does this program work for the inputs I tested?”

Static analysis asks:

“What could happen for all possible inputs?”

That difference is enormous!

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.

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.

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:

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

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!

As Rust adoption accelerates across industry, the need for advanced analysis tools becomes increasingly important.

That’s where Soteria comes in!

Soteria is a static analysis platform powered by symbolic execution.

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.

…and reasons about what could happen.

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

The result is deeper coverage, stronger guarantees and more confidence in your software.

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.

Tools built on top of the Soteria platform also use separation logic, allowing them to scale to large, industrial codebases, as analysis becomes compositional. Forget about your test harnesses: we can automatically test functions in isolation, and compose these analyses to uncover true bugs that are guaranteed to exist, reducing noise and improving productivity. Users do not need to annotate their code or write asserts, although the tool will find any such annotation helpful, of course.

Let’s now look into the technical details of how Soteria differs from the rest and why that matters. If you just want to see the results, feel free to skip ahead to the next section!

Most symbolic execution systems follow a common design. They first translate programs into an intermediate representation (IR), and then perform analysis on that representation.

In theory, this sounds elegant. One analysis engine can support many programming languages. In practice, however, this approach often introduces trade-offs. Every translation step risks losing important language-specific information. Complex language semantics become approximations. Performance suffers. Supporting advanced language features becomes difficult. And for languages like Rust, whose semantics are deliberately sophisticated, these compromises become increasingly painful.

The core idea behind Soteria is surprisingly simple:

What if we stopped translating away the language we’re trying to understand?

Soteria takes a fundamentally different approach. Instead of forcing every language through a common intermediate representation, Soteria reasons about each language on its own terms, modelling its semantics faithfully rather than approximating them through a common encoding. This means analysis can operate on the behaviour developers actually write and reason about.

The benefits are substantial:

• Greater semantic fidelity
• Support for advanced language features
• Fewer approximations
• Higher precision
• Better performance
• Easier extensibility

Rather than treating language-specific behaviour as an inconvenience, Soteria embraces it. The result is an analysis that is simultaneously more accurate and more practical, as shown in our recent publication .

Our evaluations show that Soteria enjoys industrial-scale performance, while maintaining strong semantic accuracy and discovering real bugs in production codebases.

In practical terms, that means analyses that would traditionally feel heavyweight become much easier to integrate into everyday development workflows.

The first major embodiment of this vision is Soteria Rust, a tool for analysing Rust built on top of the Soteria engine.

Rust’s ownership system is one of its defining innovations. But it is also one of the most challenging aspects for analysis tools to model correctly.

Soteria Rust is the first symbolic execution engine capable of reasoning about Tree Borrows , the leading (and still experimental) aliasing model that underpins modern Rust semantics. That may sound like a niche implementation detail, but it isn’t. Tree Borrows capture some of the most subtle aspects of how Rust references, pointers and aliasing behave. Supporting it means Soteria can reason about Rust code with a level of semantic accuracy that was previously unavailable in automated reasoning tools!

For Rust developers, that translates into:

• More accurate bug reports
• Fewer false alarms
• Better support for advanced Rust patterns
• Greater confidence when working with unsafe code

And because Soteria works directly with Rust semantics, it avoids many of the compromises that traditionally accompany language translation pipelines.

While our primary focus is Rust, we have also developed Soteria C. Systems programming remains heavily dependent on C, and many critical infrastructure components continue to be written in it.

Using the same underlying architecture, Soteria C provides compositional symbolic execution capabilities for C programs, enabling powerful reasoning about memory safety and correctness properties.

Many organisations are currently navigating mixed Rust-and-C environments. Soteria is designed with that reality in mind. Specifically, as Soteria supports both C and Rust analysis, we are working on supporting thorough analyses in mixed Rust-and-C environments with FFI. This would allow us to leverage the precision of both Soteria Rust and Soteria C, accurately analysing cross-language calls and ensuring absence of UB across the entire codebase.

Perhaps the most exciting aspect of Soteria lies beyond bug finding. Soteria doesn’t just identify bugs. It produces rich symbolic reasoning traces! These traces capture structured explanations of program behaviour, execution paths, constraints and failure conditions.

Why does that matter?

Because these traces can help teach AI systems how programs actually work. Recent research  shows that traces generated by Soteria can significantly improve a model’s ability to reason about software correctness (more on that in our upcoming post!).

This creates a powerful feedback loop:

In other words, Soteria helps verify what AI writes today, while helping build better coding AI for tomorrow.

Software engineering is entering a new era.

An era where AI writes substantial amounts of code, and verification becomes continuous. Static analysis will be integrated into every development workflow, allowing developers to receive correctness feedback instantly. Our mission is to make program reasoning automated and accessible.

To support that future, we need tools that are faster, more precise, more scalable, and more aligned with modern programming languages.

That’s the vision behind Soteria!

We’re building a platform that combines rigorous program analysis with practical developer workflows, starting with Rust and expanding beyond it. The future of software isn’t just generating more code. It’s understanding that code better. And that’s exactly what Soteria was built to do.

Whether you’re building safety-critical infrastructure, adopting Rust at scale, integrating AI into your engineering workflows, or simply trying to ship more reliable software, Soteria can help.

Join us as we build the next generation of static analysis.

Find bugs today. Teach AI to find them tomorrow.