# Exploring the Verifiability of Code Generated by GitHub Copilot

arXiv: https://arxiv.org/abs/2209.01766 · HTML: https://mlsanity.com/paper/2209.01766/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Sep 2022.

## Built on by (most cited first, 4 of 4)

- [Bugs in Large Language Models Generated Code: An Empirical Study](https://mlsanity.com/paper/2403.08937/) (2024)
- [Is AI the better programming partner? Human-Human Pair Programming vs. Human-AI pAIr Programming](https://mlsanity.com/paper/2306.05153/) (2023)
- [Turbulence: Systematically and Automatically Testing Instruction-Tuned Large Language Models for Code](https://mlsanity.com/paper/2312.14856/) (2023)
- [Numeracy from Literacy: Data Science as an Emergent Skill from Large Language Models](https://mlsanity.com/paper/2301.13382/) (2023)

## Abstract (arXiv)

GitHub's Copilot generates code quickly. We investigate whether it generates good code. Our approach is to identify a set of problems, ask Copilot to generate solutions, and attempt to formally verify these solutions with Dafny. Our formal verification is with respect to hand-crafted specifications. We have carried out this process on 6 problems and succeeded in formally verifying 4 of the created solutions. We found evidence which corroborates the current consensus in the literature: Copilot is a powerful tool; however, it should not be "flying the plane" by itself.