daitai algebraic platformdaitai大体
/

What is Formal Verification in Software Engineering?

Formal verification is the practice of proving that a program behaves exactly as specified — not for most inputs, not for the inputs you thought to test, but for every possible input, every possible state, and every possible execution path.

Most software is validated by testing: you run the program on a set of examples and check that the outputs look right. Testing is indispensable, but it is fundamentally incomplete. No test suite can cover the infinite space of possible inputs. A passing test says "this example worked once." It does not say "this property holds always."

Formal verification closes that gap. It treats the program and its specification as mathematical objects, then uses logic and automated reasoning to construct a proof that the program satisfies the specification. When the proof succeeds, the guarantee is total. When it fails, the proof obligation tells you exactly where the reasoning broke down — which is usually the exact line where a bug lives.

Why it matters now

Software has become infrastructure. It runs hospitals, markets, power grids, and spacecraft. In these domains, a bug is not an inconvenience. It is a liability. The cost of discovering an error after deployment — in money, in trust, in human harm — has grown to the point where "we tested it" is no longer a sufficient answer to "how do you know that's true?"

Formal verification is the answer. It is the difference between belief and proof.

The two worlds: model checking and theorem proving

Formal methods split roughly into two cultures:

Model checking explores the state space of a finite system exhaustively. The checker asks: "Is there any path from the initial state to a state where the property is violated?" If the search completes and finds no counterexample, the property holds for every reachable state. Modern model checkers can handle systems with billions of states, but they require the state space to be finite and the model to be explicit.

Theorem proving works with infinite or parametric systems. The prover manipulates logical formulas using axioms and inference rules to derive that the property holds for all possible instantiations. This is more expressive — it can reason about algorithms over arbitrary-sized data structures, cryptographic protocols, or concurrent systems with unboundedly many threads — but it demands more human guidance and mathematical maturity.

Both are formal verification. Both replace testing with proof. They differ in the class of systems they can handle and the degree of automation they provide.

The gap: why formal methods are still rare

If formal verification is so powerful, why is it not the default?

The traditional answer is that it is too expensive. Specifying what a program should do, in a language precise enough to prove things about, is harder than writing the program itself. The tools are esoteric. The learning curve is steep. The feedback loops are slow. Most engineering teams have deadlines.

But the deeper answer is that the programming languages themselves were not designed for proof. When a language has undefined behavior, implicit mutable state, unconstrained side effects, and no formal semantics, there is nothing solid to prove about. The program is a set of instructions for a machine, not a mathematical expression with a meaning you can reason over.

This is where the daitai philosophy begins.

Formal verification through algebra

daitai takes the position that the gap between "programs we write" and "programs we can prove" is a language design problem, not a tooling problem. If the language is built on a small, published algebra with explicit rewrite laws, then every program is already a theorem-in-waiting.

In daitai-lang:

  • Every expression has a denotation in the algebra. There is no undefined behavior because the algebra defines the meaning of every construct.
  • State change is explicit and typed through the Step relation. You cannot silently mutate something the type system did not authorize.
  • The rewrite laws are not optional optimizations. They are constitutional. The compiler, the prover, and the IDE all read the same laws.
  • There is no null. There are no exceptions. These are not conveniences; they are holes in the logical model that make proof impossible.

When you write a function in daitai-lang, you are not just writing code. You are writing a term in an algebra that already has a published equational theory. The compiler can fuse steps because the composition law is a theorem. The prover can verify monotonicity because the entropy law is an axiom. The IDE can refactor your code by applying rewrite rules that are mathematically guaranteed to preserve meaning.

Formal verification, in this view, is not a separate activity you perform after writing code. It is a consequence of writing code in a language that was designed to be provable from the first line.

When to reach for formal methods

You do not need to prove every function in your codebase. But you should consider formal verification when:

  • The cost of a bug exceeds the cost of a proof. (Safety-critical systems, financial settlement, cryptographic protocols.)
  • The system is too complex to test exhaustively. (Concurrent algorithms, distributed consensus, hardware microarchitectures.)
  • The specification itself is the product. (A compiler, a type system, a cryptographic primitive — the correctness of the implementation is the value.)
  • You need to build trust with a regulator, an auditor, or a skeptical partner who will not accept "we tested it" as an answer.

Reading next