Correctness Accelerates Innovation

The assumption has always been that rigor slows you down. The view on formal methods is that everything is 10 to 100 times slower, 10 to 100 times more expensive, 10 to 100 times more risk, based on snapshots of formal methods work from the mid-1980s. Meanwhile, businesses want to go fast, and vibe coding promises exactly that.

But once you have agents and LLMs in the loop, speed and rigor stop being at odds. They become multiplicative, because the only way to go fast with certainty, so that you're not wasting time and regularly throwing away things and refactoring code, is to actually have rigor in the artifacts as you create them. The formal methods, specs, models, and rigorous verification give you and the agents confidence to go fast.

Rework comes in many forms in engineering. Usually it's in the form of requirements changing, deciding to refactor something, or deciding to burn down technical debt. It means you spent time creating something that you may have learned from but isn't what you needed. You created the wrong thing, and now you have to evolve it, polish it, or throw it away and start over.

When you do rigorous engineering, because you think first very hard, you commonly don't build something that you didn't need**. You build exactly what you meant to build, and you show that it exactly conforms to that which you asked for.** It requires greater amounts of intellectual muscle early on, but no more intellectual muscle than you would use programming in the first place, in my experience. My teams over the past thirty years that do rigorous engineering rarely have to refactor.

Contrast that with vibe coding and some of the shallow spec-driven development tools out there. If you have just a spreadsheet of requirements and a pile of 10,000 lines of code and you decide to change 5% of your requirements, you're lost. That gap between informal language and implementation means you're sometimes better off starting over and rerunning the entire system than making a differential change. If you had formal methods-based tooling deeply integrated in your workflow, a 5% change in requirements could entail less than a 5% change in code. You and your agents know exactly what code needs to change because you would have traceability and enforcement.

Rigor makes your tasks clear, your deliverables clear, your quality and correctness and security metrics crystal clear. I've been at companies where we used lightweight formal methods and delegated the work to contractors. We would basically give them the skeleton of the code, the requirements, and a test bench with no implementations, and would say, "Please write this code." They're conforming to an existing architecture, all they have to do is fill in the pieces. Because you have the 1. technical infrastructure of code that compiles but doesn't do anything, and 2. the quality infrastructure by virtue of having a thorough test bench, you get to the end goal enormously quicker.

Whether you're delegating to human beings or to isolated AI agents with just the right context, the same principle applies. Even if you can describe an architecture with a clear diagram that's really just one view of a formal architecture spec, it gives you a mental model to work with that's enormously helpful.

Integration means you're taking pieces that were potentially separately built by different entities and putting them together, which means you have composition. That only works if the pieces were built to be compositionally assured and composed. A lot of places have enormous trouble with this: they take a big system, break it into pieces, "design" them in Microsoft Word, jump right to code, and never expose to their teammates the actual APIs and component interfaces they've built. You end up building pieces that are supposed to stick together, and only when it comes to the integration phase, which is months-long because things were inherently not composable …it's a nightmare.

Audits and certification activities—such as those I am experienced with related to standards from the FAA, NRC, DoD, NSA, and NIST—are even more striking. The average auditor gets Word documents, Excel spreadsheets, and a giant pile of partially documented code, and they're left figuring out the relationship between them. To be blunt, most of the time people get through certification by virtue of exhausting the authority, providing too much useless information until they throw their hands up. With rigorous engineering, you're giving the auditor a crystal-clear description of the system, what your assumptions are, what your threat model is. It helps them know where to focus without having to spend a lot of time and run various tools on a codebase in order to figure out where to even start.

You can be bold with vibe coding. If you can manage it, you can spin up ten instances with different prompts for the same problem, play in a handful of clones of the same git repository, or ask multiple team members to vibe code the same thing and after-the-fact compare and evaluate the outcomes. But you've created more work for yourself in order to vet those things and compare them. They don't have any baked-in metrics. They don't have any notions of quality or correctness or security. You're going to be bold and foolish at the same time.

As you might imagine given my previous two posts, this is what we are building at Sigil Logic. Our platform, currently codenamed HOARDE, coordinates AI agents that assist you in formal specs, models, with verification and traceability infrastructure behind the scenes while the developer experience stays familiar.

Now imagine you can run ten copies of HOARDE on variations on the same prompt to explore a design space in a principled fashion. Give it the product line model, say: explore the following trade-offs, give me six implementations of the following component, all of which are formally assured, but explore this design space. That's like having six top design teams working simultaneously. It really does enable that kind of boldness—not just for design, but for implementations. It boils down to alternatives and not having fear, because all the outcomes you're going to get are going to meet the quality thresholds you set. You can even ask the tool to summarize and compare the architectures of all six solutions and give you pros and cons.

Vibe coding has accelerated ideation. It helps you create codebases that you should throw away—that are going to be impossible for human beings and agents working together to actually maintain over time. If we can give people the same vibe of the experience (pun intended—I am a Dad after all!) and yet have outcomes comparable to what we have demanded for national security systems and critical infrastructure, we're in a different universe. Every line of code written from here on out could be written with rigor. That's the bet: correctness doesn't slow you down. It's what lets you actually go fast.