Draw the Lines, Let AI Color: The Future of Modular Systems

AI agents can generate functional code at blistering speeds, but fast execution does not equal sound architecture. When left to its own devices, AI lacks an intuitive sense of intermediate system representations. Instead of building modular, maintainable systems, agents generate tightly coupled, opaque solutions – a monolithic "mush" that works until it needs to be audited, updated, or debugged.

As AI renders raw execution cheap, the true value of software engineering is shifting away from writing syntax and moving toward pre-execution planning and post-execution verification. To build systems that safely evolve, formal methods are becoming an increasingly obvious, powerful choice for defining system boundaries, relationships, and requirements, letting AI fill in the details inside those safe parameters.

The Failure of Unconstrained Code Generation

In an era of rapid AI generation, developers can produce tens of thousands of lines of code without ever truly understanding the underlying structure. 

"You can now do the work without understanding the work, which was not the case when you had to write code by hand,” said Galois Research Engineer Nick Gisolfi. “You use AI and stuff comes out the other end, but no one even knows where to start trying to understand it. We used to be able to look at code and go, 'Oh, this is really disorganized. This person must not know what they’re talking about.' But that doesn’t work anymore, because AI is great at faking it."

When AI generates an entire system from scratch without explicit boundaries, verifying correctness becomes nearly impossible.

"But when you have 10,000 lines of AI-generated code and you ask, 'Is it right?' It’s really difficult to confidently know the answer,” Gisolfi explains. "Modularity reduces the aperture of what you need to look at to determine, 'Did my AI agent actually do what I asked it to do?'"  

The Coloring Book: Formal Methods as System Outlines

The alternative is to define the structure before asking AI to fill it in. Rather than generating a system as one unconstrained mass of code, engineers can use formal specifications to establish distinct components, define what each is responsible for, and precisely describe the interfaces between them. Each component thus becomes a bounded problem: As long as it satisfies its specification and interacts with the rest of the system according to its defined interface, developers don’t need to understand every detail of its implementation to reason about the system as a whole. Being able to reason about a complex system contractually takes pressure off the need to understand every line of code.

In that sense, modern system architecture can work like an adult coloring book. Formal methods and precise mathematical specifications draw the rigid, black-and-white outline of the picture – the boundaries, interfaces, and requirements for system correctness. The AI agent acts as the kid with the crayons, vibe coding “color” inside those lines.

"Sometimes the AI gives you weird results, like, 'Who the heck would put purple and yellow next to each other?'” says Gisolfi. “The code doesn’t look good, but you know that the agents respected the lines. And because we’ve used formal methods to define those lines, the system is modular, and I can move forward without caring about the details inside."

That modularity changes the verification problem. Instead of asking whether 10,000 interconnected lines of AI-generated code are correct, developers can ask a series of much smaller questions: Does this component satisfy its specification? Does it respect its interface? Do the guarantees made by one component satisfy the assumptions of the next. Have agents surfaced enough independently-verifiable evidence to support behavioral claims about a system?

When humans establish these formal boundaries, they can leverage automated verifiers to evaluate AI output against strict formal rules. As Galois Research Engineer Ryan McCleeary points out: "We have all these great tools that can check if you are satisfying XYZ on some edge. As long as you have defined your requirements, you can just throw an LLM at it and say, 'Go generate something that satisfies XYZ.' And it should be able to do it."

Human Intuition and Specification at the Edge

Importantly, creating these boundaries requires deep domain knowledge and operational context – something AI agents currently cannot replicate.

"You still need human intuition for interface design," McCleeary emphasizes. "You need a human to be able to say: 'These are the exact things that I need this system to be able to do.' I have not yet seen agents be able to do that part. The hardest part is specification. That’s where the hard work for humans still exists."

We see this exact principle in software environments like Galois’s VOXLET project, which combines neural network models with differential privacy to securely anonymize real-time speech and safeguard individual identities. Here, the team designed the system to be able to hot-swap AI speech models to fit different use cases. 

"There are models that are, for example, extremely well-trained for Russian, and others that are extremely well-trained for Mandarin,” said McCleeary. “If you need one versus another, you just go plug the right model in.”

Because the team spent the time and effort upfront to strictly define what is needed in the encoder-decoder interface, integrating new language models becomes trivial.

“Because we’ve got a good idea of the interface, it now takes only around two hours of work to plug in a new model,” said McCleeary.

Benefits

Software engineering is not disappearing. Rather, its center of gravity is moving upstream toward architecture, formal logic, and specification. When writing code becomes instant and cheap, the core engineering responsibility becomes setting terms, enforcing formal interface boundaries, and verifying results. This results in three key benefits:

• Understandability and Auditability: No one should be expected to parse tens of thousands of lines of raw AI output to trust a system. By inspecting and verifying the boundary interfaces, humans retain the ability to reason contractually over a system comprising black-box, vibe-coded components.

• Seamless System Evolution: As mission requirements shift or superior AI models emerge, developers can swap individual software or hardware components without dismantling the overarching architecture. The next-gen AI model can reimplement and optimize a single loosely-coupled component in your system, instead of the whole system.

• Bounded, Creative AI Innovation: Strict constraints provide a safe sandbox. AI agents are free to generate wildly creative, hyper-efficient implementations inside their designated box because the system logic guarantees their output cannot violate broader security or functionality boundaries.

Without human intuition guiding pre-execution planning and formal methods handling post-execution verification, AI-generated software remains an unpredictable black box. By drawing clear outlines before handing over the crayons, engineers can build systems that aren't just fast to generate, but secure, understandable, and built to adapt.

Bridging Human Intent and Machine Scale

Drawing those outlines is far easier said than done. Even as AI continues to scale system development and execution at unprecedented speeds, it is becoming increasingly clear that getting human intent into machines isn't yet a solved problem. AI agents cannot intuitively suss out the oft-unstated context, subtle domain trade-offs, or what humans truly want and need a system to do. Because specification requires humans to tell the AI what to build – a process that cannot yet be fully automated – specification is rapidly becoming the primary bottleneck to software engineering at scale.

Clearing this hurdle requires a deep, foundational mastery of how system boundaries are defined, modeled, and verified. With over 25 years of experience and expertise in formal methods, Galois has long operated at the intersection of mathematical rigor and complex system architecture. The specification problem isn't solved, but we are uniquely equipped to pioneer the research necessary to overcome it – ensuring that as AI accelerates execution, human intent remains the guiding force behind every line drawn.