Don’t Just Test It, Prove It: Verifying AI-Written Rust
Abstract
AI coding agents can write code faster than humans can meaningfully review it. Tests exercise selected cases; formal verification can establish whether specified properties hold within stated assumptions and bounds. This talk explores a workflow in which humans define the contracts, agents implement against them, and provers check the result. A hands-on comparison of Rust verification tools examines what different approaches can prove, what remains outside the proof, and the practical challenges of using them. It considers how clearly developers can express requirements and how readily the tools fit into an existing development workflow. Human judgment remains essential: a proof only helps if the specification captures the intended behavior. Attendees gain a practical basis for deciding what to test, what to prove, where to draw the boundary between verified and trusted code, and which approach fits the guarantees their project needs.
- Published in
- Proceedings of the Raptors Conference, Vol. 1 (2026)
- Conference
- Raptors Conference 2026, 21 October 2026, online
- Accepted
- 2026-09-17
- DOI
- https://doi.org/10.68495/rc.2026.C030
- Presentation
- Slides are not yet available for this paper.
- Licence
- © 2026Alexander Kalankhodzhaev. Published under Creative Commons Attribution 4.0 International (CC BY 4.0).
- Publisher
- Hackathon Raptors, Community Interest Company 15557917, London, United Kingdom
- Permanent address
- https://proceedings.raptors.dev/kalankhodzhaev-dont-just-test-it
Open access. Every entry in the Proceedings is free to read, with no charge to authors and no charge to readers. Slides are served from this site, so they stay available at the paper's permanent address.
Cite this paper
Alexander Kalankhodzhaev (2026). Don’t Just Test It, Prove It: Verifying AI-Written Rust. Proceedings of the Raptors Conference, Vol. 1 (2026). Hackathon Raptors, London. https://doi.org/10.68495/rc.2026.C030
@inproceedings{raptors2026-c030,
title = {{Don’t Just Test It, Prove It: Verifying AI-Written Rust}},
author = {Kalankhodzhaev, Alexander},
booktitle = {Proceedings of the Raptors Conference},
volume = {1},
year = {2026},
publisher = {Hackathon Raptors},
address = {London, United Kingdom},
doi = {10.68495/rc.2026.C030},
url = {https://doi.org/10.68495/rc.2026.C030},
abstract = {AI coding agents can write code faster than humans can meaningfully review it. Tests exercise selected cases; formal verification can establish whether specified properties hold within stated assumptions and bounds. This talk explores a workflow in which humans define the contracts, agents implement against them, and provers check the result. A hands-on comparison of Rust verification tools examines what different approaches can prove, what remains outside the proof, and the practical challenges of using them. It considers how clearly developers can express requirements and how readily the tools fit into an existing development workflow. Human judgment remains essential: a proof only helps if the specification captures the intended behavior. Attendees gain a practical basis for deciding what to test, what to prove, where to draw the boundary between verified and trusted code, and which approach fits the guarantees their project needs.}
}
TY - CONF TI - Don’t Just Test It, Prove It: Verifying AI-Written Rust AU - Kalankhodzhaev, Alexander T2 - Proceedings of the Raptors Conference VL - 1 PY - 2026 DA - 2026/09/17 PB - Hackathon Raptors CY - London, United Kingdom DO - 10.68495/rc.2026.C030 UR - https://doi.org/10.68495/rc.2026.C030 AB - AI coding agents can write code faster than humans can meaningfully review it. Tests exercise selected cases; formal verification can establish whether specified properties hold within stated assumptions and bounds. This talk explores a workflow in which humans define the contracts, agents implement against them, and provers check the result. A hands-on comparison of Rust verification tools examines what different approaches can prove, what remains outside the proof, and the practical challenges of using them. It considers how clearly developers can express requirements and how readily the tools fit into an existing development workflow. Human judgment remains essential: a proof only helps if the specification captures the intended behavior. Attendees gain a practical basis for deciding what to test, what to prove, where to draw the boundary between verified and trusted code, and which approach fits the guarantees their project needs. LA - en ER -