ESBMC in the
verify-rust-std Project

Context

Rust is increasingly adopted as a memory-safe systems-programming language, but most Rust applications still rely on a thin layer of unverified unsafe code in the standard library. As the AWS Open Source Blog notes, "over 90% of Rust-based products/services depend on the Rust standard library, with virtually every Rust application depending on the core library" — so any soundness gap in the standard library propagates everywhere.

AWS and the Rust Foundation launched a community effort — model-checking/verify-rust-std — to formally verify the standard library, structured as a challenge-based contest with a Tool Applications track that opened the project to additional verification backends.

Approach

Our team led the development of the GOTO Transcoder — described by the Rust Foundation as a compatibility layer originally built as a PhD research project to formalise and unify the internal representations of the CPROVER toolchain. It is released as part of the open-source ESBMC project. It lets ESBMC consume the GOTO program files that Kani already produces, so the existing Rust verification workflow can be retargeted to ESBMC's SMT-based bounded model checking engine without changes to the Rust compiler toolchain. We submitted this work through the Tool Applications track of the AWS-sponsored verification contest, which we won.

ESBMC has also been adopted as an upstream tool in the SafeTrans framework (Farrukh, Coskun, Palit and Polychronakis, ReCode '26 / arXiv 2505.10708, 2026). SafeTrans is an LLM-assisted C-to-Rust transpilation pipeline developed by researchers at Stony Brook, UC Davis and AWS that uses ESBMC to identify potential vulnerabilities in the C source before translation. Cyber-Reasoning Consultancy (CRC) is not an author of SafeTrans; the paper itself states that "this work does not relate to Baris Coskun's position at Amazon."

Results