PoP Seminar Talk

APAS-VERUS: AI Paired Proof Engineering Techniques and Experience

Brian G. Milnes, Developer
Wednesday, 13 May, 2026; 2:00pm
GHC 6501
Host: Guy Blelloch

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: can 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.

Bio

Brian Milnes has done two years of industrial AI programming languages development, followed by seven years of AI research at Carnegie Mellon School of Computer Science (SOAR). Then two years of programming research in programming languages focusing on their use in systems programming and networking (Fox Project).

Milnes was then drafted into the Internet boom and directed groups working in systems, performance, operations and architecture for Lycos, Amazon and Zillow.

M.Sc. Computer Science, University of Washington

B.Sc. Mathematics (Computer Science), Carnegie Mellon University