CSLib: Building a Platform for AI-assisted Formal Verification in Lean

Barrett, Clark

doi:10.34727/2026/isbn.978-3-85448-093-8_2

Record link:

http://hdl.handle.net/20.500.12708/230446
https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_2

Title:

CSLib: Building a Platform for AI-assisted Formal Verification in Lean

Citation:

Barrett, C. (2026). CSLib: Building a Platform for AI-assisted Formal Verification in Lean. In B. Dutertre & B. Könighofer (Eds.), Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 (pp. 2–2). TU Wien Academic Press. https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_2

reposiTUm DOI:

10.34727/2026/isbn.978-3-85448-093-8_2

CatalogPlus:

AC17999081

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Barrett, Clark

Editors:

Dutertre, Bruno
Könighofer, Bettina

Organisational Unit:

E000 - Technische Universität Wien

Series:

Conference Series: Formal Methods in Computer-Aided Design

Published in:

Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026

Date (published):

Sep-2026

Number of Pages:

Publisher:

TU Wien Academic Press

Peer reviewed:

Yes

Keywords:

formal methods; computer-aided system design; hardware and system verification

Abstract:

I’ll explain the new CSLib initiative, with a focus on its code reasoning effort, which aims to build a new industrial-strength formal verification platform in Lean for verifying real-world code. I’ll describe the principles and design decisions behind the CSLib code reasoning effort. I’ll then illustrate it with an end-to-end example that brings together: AI-assisted code generation and code specification; the Boole language and the Strata framework for language-agnostic code reasoning; trustworthy verification condition generation; and Lean automation through Lean-SMT and AI-assisted theorem proving.

Is part of:

10.34727/2026/isbn.978-3-85448-093-8

Research Areas:

Logic and Computation: 40%
Computer Engineering and Software-Intensive Systems: 40%
Computer Science Foundations: 20%

Science Branch:

1020 - Informatik: 100%

License:

CC BY 4.0