Coding agents can now produce code faster than humans can review it. Techniques that minimize the amount of code that can affect system correctness are therefore a major goal in the field. The Axon project used a coding agent to build a complete verified compiler — source language, operational semantics, optimizations, machine model, and mechanically checked correctness proofs — in 34 days under one supervisor.

The talk discusses how the project combined four validation techniques — testing, credible compilation, formal verification, and code audits - to maximize development velocity while minimizing the amount of unverified/unchecked code.

We present the overall architecture of the compiler, the roles that the different validation techniques played in the development, results from the Axon implementation, and implications for other agent centric development efforts.

see: https://arxiv.org/abs/2605.01660

Today we have thousands of apps to choose from, but it’s difficult to craft our own custom tools that do exactly what we need. Geoffrey Litt’s research explores malleable software: approaching software that feels more like a Lego set that anyone can combine to create their own tools, without programming. This talk will feature demonstrations of malleable software tools developed in contexts from travel planning to collaborative writing. It will also discuss how AI might enable a Cambrian explosion of custom tools created by non-programmers, and what kinds of new software environments will be needed to take advantage of that new power.

Great overview of Geoffrey’s work over the past few years and how LLMs could fit into the future of end-user programming.