Opinion: AI can now write code, but the possibilities go far beyond faster programming
Fabrizio Montesi, professor and centre head at the University of Southern Denmark (SDU), argues that AI's ability to write code is only the start, and that formal methods are what will make it trustworthy and more capable. He opens with an anecdote: in September 2026 an AI agent solved a hard programming task requiring university-level logic, which he had been testing monthly on AI systems for over a year. This time he had a mathematically precise proof, checked independently of the AI, that the solution met its requirements. The AI had also drawn on machine-readable computer science knowledge that did not exist when he began.
His starting point is that AI-generated code is spreading into prototypes, internal tools, bug fixes and production systems, but we cannot yet trust it. Human trust in a colleague's code comes from conversation about intent and uncertainty. An AI agent can change plan, drop approaches and reinterpret instructions repeatedly during one task, and its explanation afterwards is reconstructed from the available code and context, so it can look excellent yet mislead. AI also changes code faster than people can read it, so human review cannot scale with it.
The first wave is therefore to verify software at machine speed. Formal methods specify precisely what software must do, for example that compression never loses information, and proof assistants check proofs without using AI. One can ask AI for code together with a proof. His example is warehouse robots that must never enter the same narrow passage at once: AI writes the coordination algorithm and a proof assistant checks each version. The catch is that only what we know how to specify can be verified. This complements testing and engineering judgement rather than replacing them.
The second wave is giving AI better knowledge to program from. AI reached top levels at the International Mathematical Olympiad and has begun tackling unsolved research problems, helped by integration with the Lean proof assistant and its Mathlib library of millions of lines of precise definitions and theorems. The Lean community has begun a similar effort for computer science, the Lean Computer Science Library (CSLib), an international open source collaboration building a shared, machine-verified library of verified code and knowledge. CSLib enabled the breakthrough in his opening story.
Montesi says SDU already plays a leading role in CSLib and that several Danish universities have long-standing strength in formal methods, giving Denmark a real chance to shape what comes next.