RustyDL: A Program Logic for Rust

TL;DR

RustyDL is a novel program logic designed for Rust that enables source-level, human-in-the-loop deductive verification, facilitating proof of complex functional properties directly on Rust code.

Contribution

It introduces RustyDL, a source-level program logic for Rust, supporting interactive, deductive verification without translation to intermediate languages.

Findings

Developed a prototype verification tool for Rust based on RustyDL.

Demonstrated RustyDL's ability to verify complex functional properties.

Addressed Rust-specific challenges in program logic design.

Abstract

Rust is a modern programming language that guarantees memory safety and the absence of data races with a strong type system. We present RustyDL, a program logic for Rust, as a foundation for an auto-interactive, deductive verification tool for Rust. RustyDL reasons about Rust programs directly on the source code level, in contrast to other tools that are all based on translation to an intermediate language. A source-level program logic for Rust is crucial for a human-in-the-loop (HIL) style of verification that permits proving highly complex functional properties. We discuss specific Rust challenges in designing a program logic and calculus for HIL-style verification and propose a solution in each case. We provide a proof-of-concept of our ideas in the form of a prototype of a Rust instance of the deductive verification tool KeY.