Stop Testing, Start Proving — The Foundations of Trustworthy VibeCoding!

Come and learn about the foundations of trustworthy software and hardware development with functional programming languages such as Haskell and proof assistants such as Coq and Lean.

In the age of AI-assisted programming and “VibeCoding”, writing code has never been easier. The real challenge is knowing whether we can trust the code that was written. This is particularly important for the Internet of Things (IoT), where software increasingly interacts with humans and takes control in critical situations — from smart factories and medical devices to autonomous vehicles.

AI-assisted programming changes the economics of software development: producing code is becoming cheap, while establishing that the code is correct, secure, and conforms to its specification becomes increasingly important. Testing remains an essential engineering tool, but it can only demonstrate that a program behaves correctly for the cases we have tested. Formal verification goes further: it allows us to state what a program is supposed to do and construct machine-checked mathematical proofs that it does so.

In this lecture, we study the foundations of formal verification and its role in trustworthy AI-assisted software development. We explore how theorem provers and proof assistants can provide machine-checkable guarantees for programs, including programs generated or transformed by AI. Rather than trusting AI-generated code, we learn how to make it trustworthy by checking it against precise specifications and proofs.

The lecture gives an introduction to formally verified software development, with a special focus on programming languages, compiler construction, and programming language semantics. These foundations are essential for verifying increasingly complex software and hardware systems, from small embedded devices to cloud-scale applications.

By the end of the course, students will understand the deep connection between propositions and proofs, and between programs and types. They will be able to develop programs and machine-checked proofs in Coq and Lean and understand how formal specifications and semantics provide trustworthy foundations for software development.

The central question of the course is:

“Can we trust the program — even when an AI wrote it?”

Formal verification provides one of the most powerful answers we have.