It's time to change your thinking about Formal Methods
In boardrooms and engineering leadership meetings, formal methods still tends to get filed under "academic, expensive, not for us".
After more than a decade working in formal methods and high assurance software, I am confident that assessment is out of date. Software engineers inside your organisation are almost certainly already using formal methods in a range of ways, even if they don’t realise it. The useful question is: where on the formal methods “spectrum” your organisation should be, and how much more of it you should be relying on for the systems that really matter?
Three places your organisation is already using formal methods
If your teams write code in Java, C#, Kotlin, TypeScript, or other statically typed languages, they are using formal methods every time they compile code. Compile-time type checking is a lightweight formal-methods tool. It applies mathematical rules to code before it runs, and it stops whole categories of bugs from ever leaving a developer's laptop. Your engineering organisation has been benefitting from this for years without calling it ‘formal methods’.
If your teams write in Rust, Go, or Swift, they are also using formal methods every time they compile. Rust's compiler in particular uses techniques that came directly out of formal methods research to enforce memory-safety properties. When your ‘safe’ Rust code compiles, you have a mathematical guarantee that an entire class of memory-related security vulnerabilities cannot occur in this code.
If your CI runs a modern static analyser, that tool is doing more formal methods work on your behalf. Separation logic, symbolic execution, and abstract interpretation are the foundational basis for tools that catch defects before code reaches production — whether you and your teams have come across these names or not. This work happens on every build, invisibly, and it has become dramatically faster and more accurate in the last five years.
Why this matters
Noticing this changes how you ask about formal methods when they come up at the board level, in security committees, and in procurement and your supply chain.
You are already using formal methods, and so is every serious engineering organisation you're competing with. Formal methods tools have moved from "academic and expensive" to "invisibly embedded in modern software engineering". That shift changes the risk conversation so much that any organisation that still thinks of formal methods as something they haven't touched is already out of step with where the industry is.
When considering critical systems the interesting questions each company should be challenged with is “where on the formal methods spectrum should our critical systems should sit?” and “how far up that scale it is worth going?”
Where the spectrum runs
Formal methods is a wide spectrum. The lightweight tools that most developers already use sit at one end (type checkers, memory-safe languages, static analysis), mid-tier tools used by trained engineers on high-stakes work are in the middle (SMT solvers, protocol verifiers), and the heavyweight proof work done by specialist teams sits at the other end (interactive theorem provers, the machine-checked proofs behind projects like the seL4 microkernel).
Different stages on the spectrum have different costs and deliver different strengths of guarantee. The right band for your organisation depends on what you build and what you stand to lose if it fails.
For much product engineering, staying at the lightweight end is fine. For high-stakes systems (critical infrastructure, defence, medical, safety-critical) climbing into the middle band is more compelling than it was ten years ago, and considerably more accessible. Better tooling, shorter training windows (days rather than months), and mid-tier techniques that no longer require a formal-methods PhD have all lowered the barrier for organisations that want to reach further up the spectrum.
For a small number of systems where the stakes are highest, the top of the spectrum is the only answer and ideally the heavyweight proof work only needs to happen once. seL4 is one such piece of foundational proof work, where machine-checked proofs of correctness do not need redoing.
Kry10 OS is a commercial platform built on top of the seL4 microkernel. That means the top-of-spectrum guarantees that seL4 produces are available to your engineering teams at middle-band effort, without your organisation having to fund the proof work itself.
Next up
Kry10 is running a series on formal methods and in our next article, next up, we’ll work through what the spectrum actually looks like, where your work should sit on it, and what the cost-benefit line looks like for different kinds of systems. If you have been dismissing formal methods as a future problem, our next few pieces are for you.
---------------------------------------------------------------------------------------------------------------------
If your teams write software for critical infrastructure, formal verification is worth understanding now, not after the next incident. Find out more at kry10.com or hello@kry10.com.
Dr Martin Dehnel-Wild is Chief Scientist at Kry10. His career — across academia, government, and industry — has focussed on pulling formal verification through into the real-world systems that society depends on.