THE PROVER IS HONEST
When people fight the prover, what they're usually fighting is their own complexity.
THE ACCUSATION
Formal verification has a reputation. Too expensive. Too slow. Too academic. Requires a PhD and a research team and a budget that only aerospace can justify.
The story is always the same. We built the system. Then we tried to prove it correct. The proof effort was ten times the development effort. Therefore formal verification is impractical.
The conclusion blames the tool. The prover is too weak. The specification language is too limited. The technology is not ready.
But the prover is honest. It does not invent difficulty. It reports what it finds. And what it finds is the code you wrote.
THE HONESTY
A prover does one thing. It takes a claim about code and determines whether the claim is true for all inputs, all paths, all states.
When the claim is true and the structure is clear, the prover says: proved. When the claim is true but the structure is obscured, the prover says: I cannot determine this. When the claim is false, the prover says: no.
The prover does not struggle with correct code. It struggles with complex code. These are not the same thing.
A function that takes an input and produces an output through a clear sequence of operations — the prover handles this. A function that mutates shared state through aliased references while maintaining an invariant documented in a comment three files away — the prover cannot handle this. Not because the prover is weak. Because the reasoning is genuinely hard. For the prover. For the programmer. For anyone.
The prover and the programmer face the same problem. The prover is just honest about it.
THE COMPLEXITY
Complexity has a precise meaning here. It is not the number of lines. It is not the number of features. It is the number of things you must hold in your head to understand whether the code is correct.
Pointer aliasing. Two names for the same memory. Every write through one name invisibly affects reads through the other. To reason about one statement, you must reason about all aliases. The prover must consider all of them. So must you. You just don't notice that you're not doing it.
Implicit invariants. The linked list is sorted. The reference count matches the number of owners. The cache is consistent with the source. Nothing in the code says this. Nothing in the types enforces it. It is maintained by convention and violated by accident. The prover cannot see conventions. It sees code.
Non-local effects. The function modifies a global. The method mutates the receiver and also an object reachable through the receiver. The callback captures mutable state from three scopes up. To verify the function, you must know what it touches. When it can touch anything, you must consider everything.
Circular dependencies. A owns B which references C which calls back into A. The state of A depends on B depends on C depends on A. There is no order in which to verify the components. Because there is no order in which they are correct.
Each of these is a real engineering choice that real programs make. Each is a choice that makes the program harder to reason about. The prover quantifies this difficulty precisely: it either closes the proof or it does not. The programmer experiences this difficulty as bugs. As surprising behavior. As the system that works until it doesn't.
The prover and the programmer are fighting the same complexity. The prover fails loudly. The programmer fails silently.
THE INVERSION
The conventional approach: build the system, then verify it.
This is backwards. It is like building a house, then checking whether it satisfies the building code, then discovering that the foundation cannot support the second story.
The verification is not a phase. It is not a step that comes after implementation. The verification is a property of the engineering. Code that is well-engineered is verifiable. Code that is poorly engineered is not. Adding proof effort to poorly engineered code does not make it verifiable. It makes the proof effort expensive.
When the proof is easy, the code is simple. When the proof is hard, the code is complex. When the proof is impossible, the code is wrong.
Not wrong in the sense of producing incorrect output. Wrong in the sense of being structured so that correctness cannot be established. By anyone. By any means. The prover just makes this visible.
THE ENGINEERING
What does correct engineering look like, from the prover's perspective?
Monotonic allocation. Objects are created and never moved. Indices only increase. The thing that existed at position five still exists at position five after new things are added at positions six and seven. The prover establishes this in one step. The frame condition — what did not change — is obvious from the structure.
Structural acyclicity. Parents always have lower indices than children. Or higher. Or the graph is a tree. Or the dependency is layered. The prover terminates because the structure terminates. There is no cycle to get lost in. Because there is no cycle.
Explicit invariants. The property that must hold is stated in the type, in the precondition, in the postcondition. Not in a comment. Not in a convention. Not in the programmer's memory. The prover checks what is stated. If nothing is stated, nothing is checked.
Local reasoning. The function's behavior depends on its inputs and nothing else. The procedure's effects are described by its postcondition and nothing else. To verify a call, you read the contract. Not the implementation. Not the transitive closure of everything the implementation might touch.
Separation. This data belongs to this component. That data belongs to that component. They do not share. They do not alias. Modifications to one cannot affect the other. The prover verifies each component independently. Because they are independent.
None of these are proof techniques. They are engineering techniques. They are the choices a good systems programmer makes for performance, for maintainability, for reliability. The prover benefits from them because reasoning benefits from them.
THE FALSE TRADEOFF
The claim is that verification costs something. That you trade development speed for correctness. That you trade simplicity for safety. That the proof obligations are overhead.
This is wrong.
The precondition is not overhead. It is the statement of what must be true for the function to work. If you do not state it, callers will violate it. The precondition prevents the bug. It does not cost anything. It saves something.
The postcondition is not overhead. It is the statement of what the function accomplishes. If you do not state it, callers will assume things that are not true. The postcondition documents the contract. It does not cost anything. It saves something.
The invariant is not overhead. It is the statement of what must always hold. If you do not state it, it will be violated. The invariant prevents the corruption. It does not cost anything. It saves something.
The ghost code — the code that exists only for the proof, that is erased at compile time, that generates no runtime instruction — is free. Literally free. Zero cost in the binary. Zero cost in performance. It is pure reasoning, compiled to nothing.
The cost is not in the verification. The cost is in the complexity that makes verification hard. Eliminate the complexity and the verification is free.
THE RESISTANCE
Why do people write unverifiable code?
Because complexity is easy to create and hard to notice. Allocating a mutable reference to shared state is one line. The reasoning burden it creates is invisible until you try to verify it.
Because abstractions hide complexity. The framework manages the lifecycle. The ORM handles the mapping. The garbage collector handles the memory. Each abstraction removes something from the programmer's view. But the prover must see through abstractions. The complexity is still there. It is just hidden.
Because local decisions create global problems. Each function is reasonable. Each module makes sense. But the composition — the interactions, the shared state, the implicit protocols — is where the complexity lives. And composition is what verification must address.
Because the feedback is delayed. The complex code works today. It passes its tests. It ships. The complexity manifests as the bug next month. The race condition next year. The security vulnerability discovered by someone else. The prover gives this feedback immediately. Most people would rather not hear it.
THE QUESTION
When the proof does not close, there are two possible responses.
The first: the prover is not powerful enough. We need better tools. More automation. Smarter solvers. A bigger research budget.
The second: the code is too complex. We need simpler engineering. Clearer structure. More explicit invariants. A better design.
The first response is occasionally correct. The second is almost always correct.
The prover is a mirror. It reflects the structure of the code with perfect fidelity. When the reflection is ugly, the answer is not a better mirror.
THE PRINCIPLE
Engineer correctly and the proof follows.
Not easily. Not automatically. Not without thought. But naturally. The well-structured program has well-structured reasoning. The simple design has simple proofs. The code that a good engineer would write for performance, for clarity, for maintainability — that code is the code the prover can verify.
The code that the prover cannot verify is the code that will eventually fail in production. For the same reasons. The aliased mutation that the prover cannot track is the aliased mutation that will cause the data race. The implicit invariant that the prover cannot see is the implicit invariant that the new hire will violate. The non-local effect that the prover cannot bound is the non-local effect that will cause the cascading failure.
The prover finds these problems in minutes. Production finds them in months. The difficulty is the same. The cost is not.
Engineer correctly. The proof is not the hard part. It never was.
---
Lingenic LLC
2026