APAS-VERUS: AI Paired Proof Engineering - Techniques and Experience

Abstract

This talk focuses on my experiences using LLM AIs to generate Rust code for Acar and Blelloch’s ‘Algorithms Parallel and Sequential’ textbook. I implemented all of its 121 algorithm variants, 81 of which are parallel, and then verified them in the Verus formal verification system. This work puts to rest the question of weather current AI LLMS be used to prove practical industrial-grade, performant algorithms.
I’ll discuss my experiences, the time, the costs, and the software engineering discipline developed using programmatic techniques to drive down the agentic coding and proof costs. I’ll review Rust’s strengths and weaknesses, discuss Verus’s strengths and weaknesses and review AI agents and their interfaces.
From this work I am able to provide three metrics, which I call the CPR$: - C, a reasonable costs per lines estimate of code in agentic programming a textbook, - P, and a reasonable costs per lines of proof while proving that code and learning Verus.
The bottleneck in agentic programming and proving is now the time to review the code and proofs. I derive an exact measure, R, of how proven code reduces the cost of programmer review.