Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development

TL;DR

This paper compares credible compilation and full verification in compiler development, showing credible compilation is more efficient but verified optimizations offer stronger guarantees, with detailed quantitative analysis.

Contribution

It provides the first quantitative comparison of credible compilation versus full verification in the context of a coding agent developing a verified compiler.

Findings

Verification requires about ten times more development effort.

Verified optimizations use less efficient algorithms to improve provability.

Certificate checking time dominates proof and generation times.

Abstract

Formal program verification is a longstanding goal in the field. We present the first quantitative comparison of the two primary compiler verification approaches, credible compilation/translation validation and full verification. Working with the first verified compiler developed by a coding agent (operating under human supervision), we present quantitative results from a coding agent implementing several optimizations using these two approaches. The results indicate that 1) verification requires roughly an order of magnitude more development effort than credible compilation, 2) to enhance provability, the coding agent chooses less efficient algorithms and data structures for verified optimizations, and 3) in an attempt to minimize proof effort the coding agent repeatedly implemented optimization scope reductions for verified optimizations, and 4) certificate checking time dominates optimization and certificate generation time for the considered optimizations. Because of the increased proof overhead, verified optimizations required substantially more supervision and coding sessions than credible compilation optimizations. Given the capabilities of a modern coding agent working in this context, implementation efforts for both credible compilation and verified versions remained feasible for the considered optimizations (unreachable code elimination, dead assignment elimination, and constant propagation/folding).