Verified Implementation of the Next-gen Borrow Checking Algorithm for Rust via Abstract Interpretation

Abstract

Borrow checking is a central mechanism for Rust to ensure temporal memory safety. Its correctness is based on the intuition that the Aliasing XOR Mutability discipline guarantees that programs without borrow errors inherently could not access invalid references (i.e., pointers). However, existing work on formalizing borrow checking treats it either as a component of type systems or as symbolic execution describing resource transfer. None provides a direct explanation of the correctness of borrow checking algorithms such as Non-Lexical Lifetimes (NLL) or Polonius in the official Rust compiler that function more like static pointer analysis. We take a first step toward solving this problem by formalizing Polonius, the next-generation borrow- checking algorithm for the Rust compiler, on a core subset of Rust. We prove its correctness by showing that any program accepted by Polonius does not access invalid references at runtime. The key observation is that, when borrow checking is performed lazily, Polonius could be treated as a forward abstract interpretation on abstract domains recording pointer aliasing (borrowing) relations. By providing a concrete semantics that formally describes the Aliasing XOR Mutability discipline, we prove the soundness of this abstract interpretation, from which we derive memory safety of checked programs. This formulation of Polonius is implemented and formally verified in the abstract interpretation framework of CompCert. The correctness proofs are generated by an agentic AI under human guidance using paper proofs as proof outline. To the best of our knowledge, this is the first comprehensive formalization and verification of a borrow checking algorithm as manifested in the Rust compiler.