← All papers
A Complete, Formal Semantics for Rust Source Code
cs.PL
Oct 5, 2026 · v1
TL;DR
The core Rust semantics (Section 2) was largely mechanized in Lean 4, as described in a credited companion work by Drodt.
Abstract
Formally reasoning about Rust programs requires a rigorous formal semantics, especially in the context of deductive verification and concurrent programming. We present a modular, flexible semantics for a significant subset of (close to) source code level Rust, based on the recent locally abstract, globally concrete semantics framework, separating local evaluation of expressions from their composition into concrete traces. The semantics is extended to model Rust's asynchronous programming features and Rust's most popular async runtime, Tokio. Based on our more abstract formalization, we establish the fairness of Tokio's scheduler. Further, we show the applicability of our semantics to deductive verification of Rust by providing soundness proofs for a Rust program logic.
Problem
Deductive verification and concurrent reasoning about Rust programs need a rigorous formal semantics close to source-level Rust, including its asynchronous features.
Approach
The authors define a modular semantics for a significant subset of Rust using the locally abstract, globally concrete (LAGC) framework. Local evaluation of expressions is kept separate from their composition into concrete traces. The semantics is extended to cover async programming and the Tokio runtime. The core semantics was largely mechanized in Lean 4.
Results
Using a more abstract formalization, the authors prove that Tokio's scheduler is fair. They also show the semantics supports deductive verification by giving soundness proofs for a Rust program logic.