Formal methods are mathematically grounded techniques for proving specific properties of software, and formal verification is how that proof gets done. Instead of checking a few examples, they show in general that a program meets its specification. Functional programming is usually the foundation, because code there consists of equations and supports mathematical reasoning directly.
Key Takeaways
- Formal methods do not prove that software is “absolutely correct”. They raise redundancy so sharply that an undetected bug becomes practically impossible.
- Functional programming narrows the gap between code and mathematics: every function defines an equation, so equals can always be replaced by equals, which does not hold in imperative languages.
- Property-based testing is the first practical step toward formal methods: you state properties over all inputs using universal quantifiers instead of checking single examples, and it works in all common programming languages.
- C and C++ are considered the most dangerous programming languages, yet they run safety-critical embedded systems in cars and medical devices, where formal methods can at least secure basic correctness properties.
What Are Formal Methods in Software Development?
Formal methods is an umbrella term for mathematically grounded techniques that developers use to convince themselves that their software has certain properties. Formal verification is the core of it: proving those properties instead of sampling them. The name comes from formalization, translating a requirement into mathematical form.
The key difference from classic testing is proof instead of samples. Testing usually starts from a specification, often backed by a handful of examples. Those examples tell you what happens in exactly those cases. They tell you nothing about what happens everywhere else.
Michael Sperber explains this with a speedometer. A car drives at a certain speed, and the speedometer is supposed to show the real speed. An EU standard covers this requirement with a formula: at a given speed, the reading may deviate only by a certain margin. A certification authority does not want to be convinced by seven examples. It wants a general argument.
Formal methods deliver that argument. The formula from the standard becomes a mathematical statement, the code is translated into mathematical form as well, and a proof shows that the two match.
Correctness Is Not an End Point but Built-In Redundancy
Whether the software is then “really correct” is a question that belongs at the very end. Sperber turns it around and looks at formal methods the way an engineer would.
Every engineering discipline builds in redundancy to make a system reliable. Formal methods are a way to raise that redundancy dramatically. The safety net gets so tight that hardly any bug slips through.
People in the field call it “bombproof” or “bulletproof”. The more careful engineering view puts it more precisely: it is the most reliable method we know for convincing ourselves of software properties, and it goes many times further than testing alone.
Why Functional Programming Is Closer to Mathematics
Formal methods need a proof, and proofs run on equations. That is exactly where functional and imperative programming part ways.
In C or Java, x = x + 1 is a familiar line. Mathematically it is wrong, because x is not the same as x + 1. The line only works as an instruction: the new x is the old x plus one. There is a gap between this programming model and mathematics.
You can bridge that gap, but it takes work. Anyone verifying a C or Java program also has to deal with pointers into shared state. A change in one place can affect another. In mathematics, if x stands for 5, you can put 5 in everywhere. Equals replace equals. Imperative code breaks that rule, and it takes a lot of machinery to restore it.
Functional programming doesn’t have this problem. When you define a function, you are at heart writing an equation. That already sits close to mathematical reasoning and to what a proof needs.
Markus Schlegel adds a second angle: functional programming describes what is, the relationships in the domain. Imperative languages such as C describe how the computer should do something, step by step. Correct speed measurement in a car can be stated functionally as a property, not as a sequence of instructions.
Functional Programming Costs Less, Not More
Giving up familiar imperative constructs looks like self-denial at first. In practice, functional development is not more expensive. It is often more efficient.
One reason is the extra room for abstraction, especially in data modeling. The other is that reasoning about the program’s behavior gets simpler. Thinking about input and output is easier to keep track of than holding every state change in the right order in your head.
“I don’t really debug that much in functional programming. I just check that my function gives me the right results for the corresponding inputs.”
(Michael Sperber)
According to Sperber, studies of effort per unit of functionality consistently come out in favor of functional development. You can argue about the exact factor, but there is no loss.
Coming from university and the imperative school, you have to rethink. Schlegel describes i = i + 1 as the first stumbling block when he learned to program, because it contradicted what he knew from school math. The road to formal methods leads partly back to that way of thinking in equations.
Functional Languages Are an Ecosystem, Not a Single Language
Functional programming is not one language. It is a parallel ecosystem with its own languages, package managers and frameworks, and it has grown largely independent of the mainstream.
- Haskell is seen as the prototypical example, with a strong type system.
- Scala runs on the JVM.
- F# runs on .NET, the functional counterpart to C#, so to speak.
- Clojure runs on the Java platform.
Haskell’s strong type system is deliberate: if you write something that is likely wrong, the program won’t even compile. That strictness puts some people off. Schlegel points out that you don’t necessarily need Haskell with its monads and monoids. Clojure is functional too, without putting those hurdles up front.
Many features of modern object-oriented languages come from functional programming anyway. What they borrow has been around in the functional camp for a long time.
Formal Verification: How a Proof Is Built and Checked in Code
A proof can be written on paper, on a whiteboard or by machine. For formal methods, what counts in the end is machine checking.
Type systems are the easiest way in. A compiler already proves that a program behaves in certain ways, for example that there is no integer where a string is expected. Newer functional languages support dependent types. They let you express more of a specification directly as a type, and the type checker verifies it.
The second route is proof assistants. They work through a proof the way you would at school, only with tool support. You write the proof down in machine-readable form and have it checked. Modern tools take care of the tedious parts. Tell the assistant to do an induction over a variable, and the tool can work out the individual steps for you.
As a mature example, the two name Isabelle, a tool developed partly in Munich and in productive use for many years.
The confidence comes from the system itself. In a language with a strong type system, the program won’t compile until the proof is correct. Schlegel sums up the principle simply: when the light turns green at the end, the proof holds, and specification and implementation agree.
Proofs Belong in CI, Just Like Tests
A finished proof is code and is treated like code. Sometimes it lives in a separate file, sometimes, with dependent types, it sits right in the source code.
That means it can be versioned and wired into continuous integration. Instead of only running a test suite, the pipeline also runs the proof checker over the program and reports when something is off. The proof becomes a regular part of the pipeline, not a one-time special effort.
Formal Methods Are a Niche but Shouldn’t Be
Formal methods are seen as a niche, even though they fit almost any field. Asked what the approach is good for, Sperber answers: everything. The strengths of functional programming pay off everywhere.
Embedded development looks different in practice. C and C++ dominate there, the most dangerous languages for systems that have to work reliably, in a car or a medical device, for instance. This is where formal methods come in even below functional correctness. They check whether a program keeps its resource use within limits, whether pointer aliasing stays clean and whether the C program has well-defined behavior at all.
One practical route: develop, test and verify the software functionally, and generate the C code only after that. The generated code then stays within narrow, defined bounds.
Formal methods have existed since the 1950s, and the tools have matured accordingly. What the mainstream often lacks is simply the knowledge that all of this exists.
Three Life Hacks You Can Start With Today
Getting into formal methods doesn’t require a proof assistant on day one. Three steps work in any context.
First: write down the specification. Test cases don’t come out of thin air. They come from an idea of how the program should work. Writing that idea down explicitly is the first step, and it helps no matter which technology you use.
Second: use property-based testing. The technique comes from functional programming but is available for all common languages. Instead of single examples, you state properties over all possible inputs, for instance with a universal quantifier. That is not bulletproof yet, because the tests are generated, not proven. But it is a real step toward formal specification.
Schlegel and Sperber note that property-based testing is barely known in the testing community, even though it is a testing technique at heart.
Third: learn to think functionally. Thinking about the relationship between input and output instead of sequences of instructions cuts down on bugs during development. There is plenty of free material, and the iSAQB has put together a new curriculum on formal methods that gives an overview of the field.
Frequently Asked Questions
Why are individual test cases insufficient for verifying critical properties?
Examples only answer the question of what happens in those specific cases, not what happens in all other situations. Michael Sperber illustrates this using a speedometer: An EU standard specifies a formula for how much the reading may deviate from the actual speed. A certification authority is not convinced by seven examples but requires a general argument.
Do formal methods prove that software is error-free?
No. The more honest claim is redundancy: As in any engineering discipline, a system is safeguarded in multiple ways, and formal methods enhance this safeguarding to such an extent that an undetected error is practically ruled out. In practice, this means “bulletproof.” More precisely, it is the most reliable method known and goes many times further than testing alone.
Why is it more difficult to verify imperative code?
Because proofs depend on equations, and imperative code does not provide them. An expression like x = x + 1 is mathematically incorrect and only works as an instruction. Added to this are pointers to shared state, where a change in one place affects other places. Replacing one thing with its equivalent must first be reconstructed using a great deal of machinery.
Does functional development take more time than imperative development?
No, it is often more efficient. The article cites two reasons: additional possibilities for abstraction, especially in data modeling, and the simpler reasoning about program behavior. Thinking about input and output is more manageable than keeping every state transition in the correct order in your head. Sperber reports that he hardly ever debugs; instead, he checks the results against the inputs.
Do you have to learn Haskell to program functionally?
No. Although Haskell is considered the prototypical example with a very strict type system that prevents incorrect code from even compiling, this strictness deters some people. Markus Schlegel points out that monads and monoids aren’t strictly necessary: Clojure on the Java platform is also functional without presenting these hurdles upfront. Scala and F# are other options.
How can proofs about programs be verified automatically?
There are two approaches. Type systems are the easiest way to get started: a compiler already proves, for example, that an integer isn’t present where a string is expected, and with dependent types, more of the specification can be expressed directly as type information. The second approach involves proof assistants such as Isabelle, which was developed partly in Munich and has been in productive use for many years.
What distinguishes property-based testing from traditional example-based testing?
Instead of individual examples, one formulates properties over all possible inputs, for example using an all-quantifier. The technique originates from functional programming but is available for all common languages. It isn’t foolproof, since the tests are generated rather than proven. Nevertheless, it serves as a step toward formal specification, though it is hardly known in the testing community.
How do formal methods help with embedded software written in C?
They operate at a level below functional correctness, verifying whether a program uses resources within limits, whether pointer aliasing is handled correctly, and whether the C code exhibits well-defined behavior at all. C and C++ are considered the most dangerous languages, yet they dominate the automotive and medical device industries. A practical approach: develop, test, and verify functionally, and only then generate C code.
