@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.}
}