With AI agents doing maths, writing code, breaking out of sandboxes and into firewalls, what remedy can we reach for? Formal methods – mathematical methods for reasoning about computer code – are answering how AI can be made safe, more productive, and beneficial for all.

In this keynote, Professor Fabrizio Montesi, Director of FORM at the Danish Institute for Advanced Study and University of Southern Denmark, and Albert Jiang, Head of Formal Reasoning at Mistral AI, share their insight as international pioneers into a field that is rapidly attracting growing attention from global corporations, universities, and tech startups.

Central to this development is Lean, a technology that merges programming with mathematics, enabling computers to verify software and mathematical proofs. Using Lean, Montesi is leading a global initiative that aims to make everyday programmers and AI able to build software with mathematical confidence: CSLib, the world’s first universal infrastructure for software verification and computer science research.

Together, AI and formal methods open the door to a new generation of intelligent systems that not only code, but also prove that code works – combining creative problem-solving with mathematical certainty. The perspective extends far beyond software development:

How do we build a technological infrastructure that we can not only use, but also understand and trust?

The keynote explores the vision of a future where humans and increasingly advanced AI systems collaborate to develop reliable technology at unprecedented speed, built on the solid foundations of mathematics and computer science.