---
date: 2024-05-22
excerpts: 2
---

# Formal AI-assisted code specification and synthesis: concrete steps towards safe sociotechnical systems

## 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
[FAR Seminar](https://far.ai/labs/#:~:text=FAR%20Seminar,Labs%20community.)

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

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