<div class="csl-bib-body">
<div class="csl-entry">Barrett, C. (2026). CSLib: Building a Platform for AI-assisted Formal Verification in Lean. In B. Dutertre & B. Könighofer (Eds.), <i>Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026</i> (pp. 2–2). TU Wien Academic Press. https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_2</div>
</div>
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.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Conference Series: Formal Methods in Computer-Aided Design
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal methods
en
dc.subject
computer-aided system design
en
dc.subject
hardware and system verification
en
dc.title
CSLib: Building a Platform for AI-assisted Formal Verification in Lean
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34727/2026/isbn.978-3-85448-093-8_2
-
dc.contributor.affiliation
Computer Science - Stanford University (Stanford, US)
-
dc.contributor.editoraffiliation
Amazon Web Services
-
dc.contributor.editoraffiliation
Graz University of Technology (Graz, AT)
-
dc.relation.isbn
978-3-85448-093-8
-
dc.description.volume
7
-
dc.description.startpage
2
-
dc.description.endpage
2
-
dc.rights.holder
the author
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
2708-7824
-
tuw.booktitle
Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026
-
tuw.peerreviewed
true
-
tuw.relation.ispartof
10.34727/2026/isbn.978-3-85448-093-8
-
tuw.relation.publisher
TU Wien Academic Press
-
tuw.book.chapter
2
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
I2
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.name
Computer Engineering and Software-Intensive Systems
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
20
-
tuw.publication.orgunit
E000 - Technische Universität Wien
-
dc.identifier.libraryid
AC17999081
-
dc.description.numberOfPages
1
-
tuw.relation.ispartoftuwseries
Conference Series: Formal Methods in Computer-Aided Design
-
tuw.author.orcid
0000-0002-9522-3084
-
dc.contributor.serieseditor
Weissenbacher, Georg
-
dc.contributor.serieseditor
Hunt, Warren A., Jr.
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.editor.orcid
0000-0002-6284-380X
-
tuw.editor.orcid
0000-0001-5183-5452
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.mimetype
application/pdf
-
item.grantfulltext
open
-
crisitem.author.dept
Stanford University, United States of America (the)
