Vision Paper: Proof-Carrying Code Completions

Code completions produced by today's large language models (LLMs) offer no formal guarantees. We propose proof-carrying code completions (𝑃𝐶 3 ). In this paradigm, a high-resourced entity (the LLM provided by the server) must provide a code completion together with a proof of a chosen safety property which can be independently checked by a low-resourced entity (the user). In order to provide safety proofs without requiring the user to write specifications in formal logic, we statically generate preconditions for all dangerous function calls (i.e., functions that may violate the safety property) which must be proved by the LLM. To demonstrate the main ideas, we provide a prototype implementation in the program verification language Dafny, and a case study focusing on file system vulnerabilities. Unlike Python code generated by GPT-4, Dafny code generated by 𝑃𝐶 3 provably avoids a common weakness related to path traversal (CWE-35), using a single generation attempt (𝑘 = 1) and a modest number of tokens (3, 350). Our tool is available as an open source repository at https://github.com/DavisPL/PCCC . CCS Concepts • Software and its engineering → Formal software verification; Software development techniques; Formal methods.