Global Initiative Aims to Bring Mathematical Certainty to Modern Software and AI
The University of Southern Denmark plays a leading role in a new international initiative, CSLib, which aims to build a shared formal infrastructure for developing software with mathematical guarantees.
Modern societies are deeply dependent on software. From energy systems and public infrastructure to healthcare, scientific research, and communication, software plays a crucial role. At the same time, artificial intelligence is increasingly used to generate and improve code. This makes methods for improving the reliability, security, and transparency of software more important than ever.
Within computer science, mathematical techniques already exist to precisely describe and verify software – known as formal methods. However, this knowledge is currently scattered across research papers and specialized tools, making these methods difficult to apply broadly in mainstream software development.
The new international initiative CSLib aims to change that. Its goal is to turn formal methods into a shared, reusable infrastructure for software development. The initiative brings together researchers and experts from institutions including the University of Southern Denmark, Stanford University, the University of Texas at Austin, Amazon, Google DeepMind, and the Lean FRO.
For the University of Southern Denmark, participation in the leadershop of CSLib places the university at the center of efforts to shape the future foundations of software and artificial intelligence.
The initiative builds on ongoing research at SDU in formal methods, distributed systems, and secure software, while enabling researchers and students to collaborate closely with leading international research environments in the field. The project is also aligned with the University of Southern Denmark’s strategy to strengthen international research collaboration and develop strong research and innovation environments.
Professor Fabrizio Montesi, Director of the Centre for Formal Methods and Future Computing (FORM) and Chair at the Danish Institute for Advanced Study (DIAS) at the University of Southern Denmark, serves as Lead Maintainer and member of the initiative’s Steering Group.
”Software now operates at planetary scale. To achieve trustworthy digital systems – including those shaped by AI – we need mathematical clarity that is equally far-reaching”, says Montesi, “CSLib is long-term architectural work: building the shared intellectual infrastructure on which future computing will stand.
According to Montesi, the ambition is not only to produce new research results, but also to create a shared infrastructure that researchers and developers around the world can build upon.
Mathematical building blocks for the software of the future
CSLib aims to formalize central areas of computer science - including algorithms, programming languages, and distributed systems - in the programming language and digital proof assistant Lean. Lean makes it possible to verify software mathematically using proofs that are checked by a computer.
”Lean gives us a language where software and its mathematical specification live side by side. What has been missing is a shared, composable library of verified building blocks that practitioners can actually reach for. CSLib is exactly that missing layer.
The goal is to build a large library of verified components and mathematical specifications that both researchers and developers can use to build reliable systems.
For research, this means that new results can be more easily reused and built upon, rather than each research group having to develop their own formal models from scratch. This can accelerate progress in areas such as software theory, security, and artificial intelligence.
Artificial intelligence increases the need for verified software
The project is being launched at a time when AI systems are increasingly able to generate and optimize complex codebases on their own. This can accelerate innovation - but it can also allow errors and vulnerabilities to spread more quickly. For this reason, computer-verified mathematical reasoning is becoming an important part of the foundation for future software.
”CSLib will provide mathematically rigorous guardrails for AI-driven software development, providing one blueprint for how humans and AI can work together safely for the benefit of humanity.
At the same time, researchers point out that AI-generated code makes the need for formal verification even more evident. When software can be produced at a much higher speed than before, it becomes crucial to also have methods that can automatically check whether the code actually behaves correctly and securely.
”I am most excited about the potential of CSLib to accelerate formal verification of AI-generated code. AI coding agents are notorious for generating insecure code. Formal verification is a gold-standard way of making code secure by construction, but it requires infrastructure for modeling the mathematical meaning of code. CSLib will be the first universal infrastructure for this kind of modeling.
By integrating formal verification directly into the way software is designed and developed, the ambition is for CSLib to help strengthen trust in digital systems in the decades to come.
For SDU, the project opens up new opportunities for international research collaborations, joint innovation projects, and talent development in a field that will play an important role for both technological development and society’s digital infrastructure.
CSLib is an open, collaborative initiative, and researchers, developers, and institutions from around the world are invited to contribute to its development.