| AI is revolutionizing the way code is written, but with more and more AI-generated code, the dangers of AI-introduced bugs and vulnerabilities are also increasing. At the same time, AI has also dramatically increased the capabilities of malicious actors, making even existing code more vulnerable. Fortunately, there is hope. The same GenAI power also shows promise in helping write formal specifications and in creating proofs, thus lowering the bar for formal verification. This leads naturally to a vision of a future in which AI only generates fully verified code. Achieving this ambitious goal will require a massive coordination of effort among stakeholders in academia and industry. CSLib is a new project which aims to catalyze this effort. There are two main pillars in CSLib. The first is an effort to formalize the core theoretical concepts of computer science in the Lean theorem prover. This can be seen as a sister project to the MathLib initiative, which aims to formalize mathematics in Lean. The second pillar is unique to CSLib. The goal is to build a trustworthy platform for formally verifying code in commonly used programming languages (e.g., C/C++, Python, Rust, etc.). CSLib introduces a new intermediate verification language (IVL) called Boole, partly inspired by the well-known Boogie language, a highly-successful IVL used by tools such as Dafny. However, Boole differs in two significant ways. First, it extends Boogie’s capabilities significantly. And second, it is embedded in Lean, allowing us to leverage Lean to reason about Boole programs. The Boole ecosystem is guided by several forward-looking design principles, which aim to avoid difficulties encountered in previous verification frameworks: (i) Boole looks like pseudocode and is easy for humans (and natural language-based AI tools) to understand; (ii) Boole and its ecosystem are embedded in Lean with the goal of minimizing the trusted computing base (TCB); (iii) verification conditions are generated as Lean goals, opening the door to a variety of automated proof techniques; and (iv) code specifications can leverage the formalizations from Pillar 1. Boole also leverages the Strata framework for defining deeply embedded languages in Lean.1 In the talk, I’ll explain CSLib in more detail, focusing on the code reasoning (pillar 2) effort. I’ll mention current active areas of research in the CSLib project and 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. |