Today, translating general Rust code to formal languages such as Rocq or Lean is practically working with "rocq-of-rust". By general Rust code, we mean arbitrary safe Rust, or "safe" unsafe Rust (for now). This means that one can take a Rust program and translate it into a formal language, preserving the source code as is, along with all the optimizations, which are often critical in Rust projects. As a result, you can formally verify any security properties and business rules, including for complex cryptographic libraries or programs with many external dependencies, for example. One example is our ongoing verification project for Revm, a Rust implementation of the Ethereum virtual machine designed, among other things, to run on future zkVMs where security is critical. How is the "rocq-of-rust" approach unique? We do a 𝒅𝒆𝒆𝒑 𝒆𝒎𝒃𝒆𝒅𝒅𝒊𝒏𝒈 of the Rust language in Rocq (from THIR level). This means taking the syntax tree type from the Rust compiler and implementing it on the Rocq side (without extra information like line numbers), with semantic rules to evaluate each node. As this translation is very "one-to-one", it can import a large amount of Rust code, like the "core" library or most programs we tried it on. For formal verification, the simplest representation is 𝒔𝒉𝒂𝒍𝒍𝒐𝒘 𝒆𝒎𝒃𝒆𝒅𝒅𝒊𝒏𝒈. So here comes the second step: we provide a proof framework to show the equivalence between the deep embedding and a shallow embedding. This step heavily relies on automation and AI and is safe because formally verified. As of today, the translation speed to shallow embedding is about "one file per day" (very rough estimate), which we think is acceptable compared to the time spent verifying each file to prove typical specifications. As a bonus, we do not rely on the borrow checker, even if it helps to have structured Rust programs as inputs. So this means this approach should work as well for C or Go code. We believe the use of a "deep-embedding + automation with AI to a shallow-embedding" is an interesting new combination for translating complex imperative code into formal languages, with both wide support for inputs and high-level outputs for complex verifications. Note that this work is still in progress, and we welcome any remarks/fixes. For Lean users, the last translation step from Rocq to Lean can be done through an extraction mechanism, given that the two languages are very similar on the computational part (straightforward, but to be implemented), or using "rocq-lean-import", which works much better than its humble README suggests, especially for computations. We are happy to discuss with you if you have large Rust code that you want to secure with the largest possible scope. Below is a link to the work on Revm 👇