Expanding the Rust Formal Verification Ecosystem: Welcoming ESBMC
The Rust Foundation is excited to celebrate the successful integration of a new formal verification tool, ESBMC (Efficient SMT-based Context-Bounded Model Checker), into the Rust standard library verification initiative.
This exciting achievement was realized by the team behind the Goto-Transcoder project, who submitted their work through the Tool Applications track of the AWS-sponsored standard library verification contest. The Rust Foundation was delighted to be asked by AWS to host this contest back in November.
This winning contribution adds ESBMC—a state-of-the-art bounded model checker—to the suite of tools used to analyze and verify Rust’s standard library. By integrating through Goto-Transcoder, they enabled ESBMC to operate seamlessly in the Rust verification workflow, significantly expanding the scope and flexibility of verification efforts.
The workflow is now live and running in the project’s CI:
https://github.com/model-checking/verify-rust-std/pull/236
ESBMC is now officially listed in the Approved Tools section of the Verify Rust std book, joining a growing community of tools helping to make Rust even safer through formal methods. Please join us in congratulating the ESBMC + Goto-Transcoder Team for winning this exciting cash prize!
Beyond the Contest: ESBMC’s Expanding Role in Rust Verification
This achievement builds on years of ongoing collaboration across the Rust and formal verification communities. The foundation for this work was laid during early technical exchanges between members of the ESBMC team and key contributors to Rust verification tools. Discussions around Kani’s contract system (implemented at the GOTO-program level of CBMC) sparked the idea that ESBMC could similarly support Rust verification if a compatibility layer could be developed.
That insight led to the creation of Goto-Transcoder, originally developed as part of a PhD research project aimed at formalizing and unifying the internal representations of the CPROVER toolchain. When the Rust standard library verification initiative launched, this work provided the perfect starting point for a meaningful contribution.
The collaboration has since expanded. In addition to verifying the Rust standard library, the team is exploring the use of formal methods to validate automated C-to-Rust translations, with support from AWS. This direction, highlighted by AWS Senior Principal Scientist Baris Coskun and celebrated by the ESBMC team in a recent LinkedIn post, represents an exciting new frontier for Rust safety and verification tooling.
Looking ahead, the team is working to expand ESBMC’s support for contract constructs and aiming to integrate it as an alternative backend for Kani—bringing deeper alignment across the CPROVER ecosystem and unlocking new capabilities for Rust developers using SMT-based tools.
Q&A with the ESBMC + Goto-Transcoder Team
We spoke with Rafael Menezes – a member of the team behind this successful integration to learn more about their approach, the challenges they faced, and what comes next:
Q: What inspired you to contribute to the Rust std-lib verification initiative?
A: I’m currently working on my PhD thesis, which involves formalizing the inner workings of the CPROVER tools and conceptualizing a unified intermediate language. From that effort, the Goto-Transcoder was born. When Felipe learned about this, he mentioned the attempt to verify the Rust standard library, which led to this contribution.
Q: Can you explain what ESBMC is and how it differs from other tools in the verification flow?
A: ESBMC originated from the PhD project of my PhD supervisor, which began as a fork of CBMC, focusing on the verification of concurrent programs and utilizing SMT solvers. Furthermore, ESBMC can now explore other techniques, such as proof by induction.
Q: What was the biggest technical challenge in integrating ESBMC into the Rust ecosystem?
As mentioned before, Kani’s intermediate language can be used as an input to ESBMC. The main challenge is that, although they were a fork, the tools evolved in different ways. For this reason, we had to adapt and extend ESBMC to support certain behaviors from CBMC. It was a challenge, but a fascinating one to tackle!
Q: How do you ensure the correctness and soundness of the verification results?
For the translation of the program itself, we rely on Kani for correctness. Our tool works by transforming the program into bounded traces, which are then converted into an SMT formula. The formula is encoded in a way that if there were any violation of the program, it would result in a counterexample that can be used to replicate the problem.
Q: How do you see ESBMC contributing to Rust’s long-term safety and reliability?
First, by ensuring that the standard libraries are doing what we expect them to be doing. Then, by bringing another software verifier that supports Rust. Both carve a path to improve the development of safer software, which I think all of us in the open source ecosystem can agree is crucial.
Q: What advice would you give to other teams that want to get involved in Rust formal verification?
Get in contact with the team in the repositories! They are a very helpful bunch, always dedicated to solving any issues.
Q: How was your experience working with the Rust verification community and the AWS initiative?
It was great! The AWS team was tremendously helpful. They even set up meetings to provide us with technical advice on how to proceed. We felt very supported and inspired throughout the entire process.
Q: How do you feel the Rust community is receiving this work?
I feel like the Rust community is very appreciative of tooling, especially the ones that regard safety—all our posts in the community were highly commented on, which was heartening to see.
Q: What’s next for the Goto-Transcoder Project?
In short, we are focusing on supporting more contracts and thoroughly verifying the Rust standard library through our efforts. We’re excited to keep working towards this!
