In this era of AI-driven development most approaches still involve a human in the loop for reviewing the code, participating in the testing, or a combination. The spec-driven movement is no exception.

Until recently, AI-driven development was at a pace, where humans could keep up. But with the emergence of agents, the scope and speed of development increase so rapidly that, in some cases, exhaustive human review or test participation is not realistic.

How can we have faith in the coding and testing done entirely by agents?

We present some recent agent-driven development projects which involve thousands of changes to a code base, which make human validation unrealistic.

A central aspect of the approach is that we do not let the agent do things, instead we let the agent create algorithms that do things. Also, we let the agent create tests - or algorithms that create tests - which can be executed without human involvement.

It can be observed that the artefacts created during development are a kind of pipelines rather than traditional code, making the developer more of a devOps than classical coder.

The projects have been released to production with so far no incidents being reported.

We will end by looking towards the future and relate the experiences gained in the projects to the recent advances in the maturity of proof assistants and solving open math problems with agents.

Bio

Morten Heine Sørensen is a computer scientist and software developer.

He holds a PhD in Computer Science from the University of Copenhagen, where he was an assistant professor and researcher in programming languages, program transformation, lambda calculus and type theory. His academic work includes more than 50 research papers and a book on the Curry–Howard correspondence between programs and proofs.

As a developer, he has 25 years of experience building mission-critical software systems. He has worked hands-on as developer on large-scale systems across finance, government, energy and other sectors.

He has substantial experience with usage of generative AI and AI-driven software development working extensively with AI-based code generation.

His current work brings these three strands together: practical large-scale AI-driven software engineering, the more formal question of how we can establish confidence in software produced with little or no human involvement, and the use of Generative AI to prove theorems and use proof assistants to validate the proofs.