---
date: 2024-05-08
excerpts: 2
---

# AI-assisted coding: correct by construction, not by generation

## Abstract

Atlas and Topos has been working on a roadmap for AI-assisted code specification and synthesis. The thesis is that formal verification (FV) is our best bet for protecting our sociotechnical systems, especially from human-led and/or AI-enabled attacks. Formal AI-assisted coding could make FV widespread and turn the tide in favor of defense. The roadmap describes concrete projects towards that goal. In this talk, I will discuss various components of the roadmap and show simple demos of what language models can do out of the box. I will also dive into correct-by-construction code synthesis, and how that it preferable to token-by-token code generation.

## Details
[Topos-Chapman Workshop](https://blogs.chapman.edu/scst/announcement/chapman-university-to-partner-with-topos-institute/)

[Video](https://www.youtube.com/watch?v=rHY7nboIyBg)

[Slides](https://w3id.org/people/shaoweilin/public/20240508-chapman.pdf)