> Markdown version of [/videos/720-when-testing-just-doesn-t-cut-it?t=4](https://www.wearedevelopers.com/videos/720-when-testing-just-doesn-t-cut-it?t=4). Every page supports `.md` or `Accept: text/markdown`. Links point to the HTML versions so they work for humans too. Agent guide: [/agents.md](https://www.wearedevelopers.com/agents.md).

---

# When testing just doesn’t cut it

Even the Java JDK hid longstanding bugs despite heavy unit testing. Learn how high-stakes systems use mathematical proofs to guarantee flawless code before a single line is written.

- **Speakers:** Lars Hupel
- **Event:** World Congress 2023
- **Published:** September 27, 2023
- **Duration:** 27:54
- **URL:** https://www.wearedevelopers.com/videos/720-when-testing-just-doesn-t-cut-it

## Summary

While modern software relies heavily on unit testing and high code coverage, these practices are inherently inadequate for proving the true absence of bugs. Even highly vetted standards, such as the Java JDK's binary search, have suffered from longstanding integer overflow defects because traditional unit testing rarely uncovers extreme edge cases. To build absolute certainty in software—especially in life-critical or high-stakes domains—engineering teams turn to formal methods. While everyday tools like flowcharts and static type checking in TypeScript represent basic forms of structured syntax, formal verification takes this concept further by using mathematical proofs to guarantee an implementation flawlessly matches its specification.

This mathematical rigor is essential in industries like aerospace, medicine, and finance. When building complex systems like Central Bank Digital Currency (CBDC), organizations cannot afford architectural flaws that might allow users to duplicate offline currency through smart devices. By leveraging the Isabelle theorem prover, software and architecture teams can express business rules in a functional programming syntax and guarantee system invariances, such as ensuring the total money in circulation stays perfectly constant across distributed networks.

Because formal verification is highly resource-intensive—often requiring ten lines of mathematical proof for a single line of executed code—pragmatic application is a necessity. Instead of attempting to verify entire existing codebases, teams prioritize prototyping novel functionalities and complex state interactions within Isabelle first. This strategic approach catches dangerous edge cases before engineers translate vetted models into production-ready Go or JavaScript, efficiently bridging the gap between unreliable testing assumptions and mathematically proven software safety.

**Keywords:** software testing limitations, integer overflow bugs, java binary search defect, formal methods, formal verification, mathematical code proofs, software specification, static type checking, isabelle theorem prover, central bank digital currency, CBDC software architecture, bug prevention strategies, high-stakes software engineering, feature prototyping, edge case detection

## Chapters

1. **Missed edge cases in standard unit testing** (00:04) — How traditional unit testing often misses critical edge cases like integer overflows in standard algorithms.
1. **Defining formal methods for software verification** (05:02) — Defining formal methods as mathematically rigorous techniques for software specification and validation.
1. **Everyday examples of formal methods in engineering** (06:20) — How standard tools like flowcharts and static type systems act as fundamental formal methods.
1. **Understanding formal verification processes in practice** (09:43) — Ensuring code implementations match mathematical specifications by writing proofs alongside assertions.
1. **Preventing catastrophic failures in high-stakes software** (14:03) — Why aeronautics, healthcare, and finance require methods beyond testing to prevent life-threatening or costly bugs.
1. **Modeling and verifying rules for digital currency** (17:12) — Representing physical money rules in code to mathematically prevent unauthorized duplicate transactions offline.
1. **Proving strict system constraints using Isabelle** (20:31) — Using the Isabelle theorem prover to mathematically guarantee system invariants stay constant.
1. **Integrating theorem provers into the development workflow** (23:07) — Prototyping complex new features with formal proofs before implementing them in production languages.
1. **Audience questions on writing effective software specifications** (26:06) — Addressing questions about pull requests, deriving programs from specifications, and covering essential edge cases.

## Related Moments

- [State of the art in software verification](https://www.wearedevelopers.com/videos/1644-ai-meets-hoare-logic-revolutionizing-software-testing-with-formal-methods) (from "AI Meets Hoare Logic: Revolutionizing Software Testing with Formal Methods")
- [Comparing software testing and software verification](https://www.wearedevelopers.com/videos/1644-ai-meets-hoare-logic-revolutionizing-software-testing-with-formal-methods) (from "AI Meets Hoare Logic: Revolutionizing Software Testing with Formal Methods")
- [Raising awareness for software verification](https://www.wearedevelopers.com/videos/1644-ai-meets-hoare-logic-revolutionizing-software-testing-with-formal-methods) (from "AI Meets Hoare Logic: Revolutionizing Software Testing with Formal Methods")
- [Automating broad codebase validations via consistent type level constructs](https://www.wearedevelopers.com/videos/455-where-we-re-going-we-don-t-need-javascript-programming-with-type-annotations) (from "Where we're going we don't need JavaScript - Programming with Type Annotations")
- [Treating software testing as an experimental and undecidable science](https://www.wearedevelopers.com/videos/87-excellent-software-testing) (from "Excellent Software Testing")
- [Different forms of software testing](https://www.wearedevelopers.com/videos/222-test-driven-development-with-javascript) (from "Test Driven Development with JavaScript")

## Related Articles

- [Now is the time for industrialized software development](https://www.wearedevelopers.com/magazine/601-now-is-the-time-for-industrialized-software-development)
- [How to Avoid Over-Engineering](https://www.wearedevelopers.com/magazine/546-how-to-avoid-over-engineering)
- [Dev Digest 138 - Are you secure about this?](https://www.wearedevelopers.com/magazine/486-dev-digest-138-are-you-secure-about-this)
- [Dev Digest 101 - the XXX edition](https://www.wearedevelopers.com/magazine/382-dev-digest-101-the-xxx-edition)

## Related Jobs

- [Senior Software Engineer](https://www.wearedevelopers.com/jobs/ext/15942-senior-software-engineer) at **GitHub**
- [Principal Software Engineer, Identity](https://www.wearedevelopers.com/jobs/ext/1469181-principal-software-engineer-identity) at **GitHub**
- [Principal Software Engineer, Enterprise AI Platform](https://www.wearedevelopers.com/jobs/ext/1467292-principal-software-engineer-enterprise-ai-platform) at **GitHub**
- [Test Engineer](https://www.wearedevelopers.com/jobs/ext/1872489-test-engineer) at **ZEISS Group**
- [Engineer, Offensive Security Organization](https://www.wearedevelopers.com/jobs/ext/1992296-engineer-offensive-security-organization) at **Twilio**
- [Senior Software Engineer, Enterprise Products](https://www.wearedevelopers.com/jobs/ext/1841248-senior-software-engineer-enterprise-products) at **GitHub**