A Proof Cannot Rescue the Wrong Problem

Formal proof is powerful because it replaces a kind of hope with a mechanical answer. State a property precisely, provide a valid proof, and a checker can establish that the program satisfies that property. That is much stronger than asking a reviewer whether the code looks right or trusting a demo that happened to work once.

But the checker begins where the specification begins. It does not know whether the property matters to the customer, whether the model leaves out a dangerous behavior, or whether a mature solution already handles the problem better. It proves the statement you gave it. It does not prove that you asked the right question.

That boundary matters more when agents can produce an implementation, a proof, documentation, and a polished demonstration in one burst. The package arrives looking complete. Completeness inside the chosen frame can hide that nobody challenged the frame itself.

A person building an unfamiliar system used to hit friction early. The missing knowledge showed up as a blank editor, a failed design discussion, or weeks of implementation. That friction was expensive, but it sometimes forced the team to study the field before committing to an approach.

Agents remove much of that pause. Give one a plausible design and it can turn the design into a working artifact before anyone has compared alternatives, inspected prior art, or tested the premise. Speed makes the first coherent answer feel like a discovery when it may only be the first route the agent could finish.

This is the real danger in vibe coding. It is not merely that generated code may contain bugs. Bugs can face tests. The deeper failure is building a confident solution before doing enough work to learn that the solution is obsolete, misframed, or aimed at a problem the business does not need solved.

The answer is not a longer pause or a committee that blesses every idea. Research should be a factory stage with a contract. Before implementation starts, the route should identify the decision being made, find credible alternatives, record why they do or do not fit, name the unknowns that could reverse the choice, and state what evidence permits the work to advance.

An agent can do most of that repeatable labor. It can search documentation, compare mechanisms, reproduce claims, inspect existing implementations, and assemble the evidence. A separate gate can reject thin sourcing, missing alternatives, or a recommendation that never tested its strongest objection. Human judgment owns the consequence and chooses among genuine tradeoffs.

The output is not a pile of links. It is a decision record the next stage can consume: this is the problem, these are the constraints, these approaches were examined, this one was chosen for these reasons, and this evidence would make us change course. That record keeps implementation from laundering an untested premise into a finished-looking product.

Once a route is selected, proof still needs an independent specification. Do not let the builder quietly define success from the artifact it already produced. The requirement should come from the decision record and describe the consequence that must hold, not the easiest property the implementation can prove.

Then attack the omissions. What happens outside the formal model? Which runtime, compiler, integration, or operator sits beyond the theorem? Which customer behavior was simplified away? A proof can be valid while the surrounding system fails because the trusted boundary was larger than anyone admitted.

This does not diminish formal methods. It gives them an honest job. Use proof to make important properties mechanically unavoidable. Use tests and production observation for conditions the model does not cover. Use research and accountable judgment to decide which properties and mechanisms deserve the investment in the first place.

As implementation gets cheaper, the valuable human decision moves earlier. People should not spend their days typing a design into existence or manually repeating a literature search. They should decide what outcome matters, what evidence changes the decision, and which consequences the factory may accept.

That shift will eliminate work built around carrying an unquestioned plan through implementation, review, and release. Agents can perform those repeatable steps faster and retain the process in machinery. The jobs that remain will sit closer to choosing the destination and governing the boundaries, not supervising every keystroke along the way.

Our position is simple: the factory must be able to refuse a well-built answer to a badly chosen problem. Research the premise. Challenge the route. Write the specification independently. Then use every test and proof available to hold the implementation to it. A perfect certificate on the wrong destination is still a wrong turn.