In this excerpt from Elektor Engineering Insights #54, I asked Quentin Ochem from AdaCore the obvious-but-annoying question: why can’t we just do software testing for everything and be done with it?

As Quentin points out, even a tiny function with two integers would take an astronomical number of test cases to cover every possibility. You’d be testing until the heat death of the universe and still miss something. Coverage metrics, fuzzing, boundary analysis — they all help, but none of them can prove correctness.
 


Formal verification, on the other hand, actually can. With SPARK, you can mathematically prove your code does what the specification says in 100% of cases. That level of certainty might be overkill in safety, where “nine-nines” reliability can be good enough depending on cost. But in security, attackers only need one exploit in ten million lines of code, so proof beats probability every time.

Quentin also mused about AI joining the party — not replacing static analyzers, but augmenting them with new ways of spotting bugs and maybe even suggesting fixes. I told him I’ll believe it when my IDE stops nagging me about missing semicolons.
 

Have Your Say: Software Testing vs. Formal Verification

Formal verification might sound like academic overkill, but Quentin’s point is clear: when attackers only need to find one bug, the odds are stacked against you if you rely on testing alone. Tools like SPARK shift the argument from probability to certainty, and that raises questions for everyone writing code — from embedded engineers to software teams under constant pressure to ship. I’d like to know what you think: is proof the future, or will most of us still settle for “tested enough”? Share your thoughts in the comments.

Subscribe
Tag alert: Subscribe to the tag Elektor Engineering Insights and you will receive an e-mail as soon as a new item about it is published on our website!