Paper
RustyDL: A Program Logic for Rust
Authors
Daniel Drodt, Reiner Hähnle
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.
Metadata
Related papers
Fractal universe and quantum gravity made simple
Fabio Briscese, Gianluca Calcagni • 2026-03-25
POLY-SIM: Polyglot Speaker Identification with Missing Modality Grand Challenge 2026 Evaluation Plan
Marta Moscati, Muhammad Saad Saeed, Marina Zanoni, Mubashir Noman, Rohan Kuma... • 2026-03-25
LensWalk: Agentic Video Understanding by Planning How You See in Videos
Keliang Li, Yansong Li, Hongze Shen, Mengdi Liu, Hong Chang, Shiguang Shan • 2026-03-25
Orientation Reconstruction of Proteins using Coulomb Explosions
Tomas André, Alfredo Bellisario, Nicusor Timneanu, Carl Caleman • 2026-03-25
The role of spatial context and multitask learning in the detection of organic and conventional farming systems based on Sentinel-2 time series
Jan Hemmerling, Marcel Schwieder, Philippe Rufin, Leon-Friedrich Thomas, Mire... • 2026-03-25
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2602.22075v1</id>\n <title>RustyDL: A Program Logic for Rust</title>\n <updated>2026-02-25T16:25:04Z</updated>\n <link href='https://arxiv.org/abs/2602.22075v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2602.22075v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>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.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.PL'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.LO'/>\n <published>2026-02-25T16:25:04Z</published>\n <arxiv:comment>Long version of paper published at 27th International Symposium on Formal Methods (FM 2026)</arxiv:comment>\n <arxiv:primary_category term='cs.PL'/>\n <author>\n <name>Daniel Drodt</name>\n </author>\n <author>\n <name>Reiner Hähnle</name>\n </author>\n </entry>"
}