Copper: Unifying Correctness and Performance Specification in Code Generation
2026-07-03 • Software Engineering
Software Engineering
AI summaryⓘ
The authors introduce Copper, a system that helps AI generate computer code that is both guaranteed to work correctly and runs efficiently. They combine AI code creation with formal checking methods and performance testing to make sure the code is reliable and fast. When tested on different programming tasks, Copper made programs that were more trustworthy and used less time and memory than typical AI-generated code. This shows it's possible to produce AI-written code that you can trust and that performs well.
Generative AIFormal VerificationCode SynthesisPerformance ProfilingRuntime EfficiencyMemory EfficiencyAI-Assisted ProgrammingCorrectness GuaranteesAlgorithmic TasksAutomated Testing
Authors
André Lizardo, Raul Barbosa
Abstract
Generative AI has made remarkable progress in producing functionally correct code, yet ensuring both correctness and performance remains an open challenge. We present Copper, a framework that combines formal verification with performance-aware specification to generate code that is provably correct and efficiently executable. Our approach integrates AI-driven code synthesis with formal verification tools, and automated performance profiling loops. Evaluated on a diverse set of algorithmic and real-world programming tasks, Copper produces solutions that satisfy strict correctness guarantees while delivering significant improvements in runtime and memory efficiency compared to baseline AI-generated code. This work demonstrates that it is feasible to bridge the gap between trustworthiness and performance in AI-assisted programming, offering a practical pathway toward reliable, high-performance code generation.