When testing just doesn’t cut it

How do you find a bug that lets users duplicate money before writing a single line of code?

#1about 5 minutes

Why high code coverage is not enough

Even well-tested software like Java's JDK can have critical bugs, such as the famous integer overflow in binary search, demonstrating the limits of unit testing.

#2about 1 minute

Defining formal methods for software verification

Formal methods are mathematically rigorous techniques for specifying, designing, and verifying software systems, used by organizations like NASA to ensure correctness.

#3about 4 minutes

Recognizing formal methods in everyday tools

Common tools like standardized flowcharts and static type systems in languages like TypeScript are practical examples of formal methods already in use.

#4about 5 minutes

How formal verification proves code correctness

Formal verification involves creating a mathematical proof that a software implementation correctly adheres to its formal specification, going beyond simple testing.

#5about 5 minutes

Applying formal methods to central bank digital currency

Building a Central Bank Digital Currency (CBDC) requires a higher level of assurance than testing can provide to prevent financial loss or money duplication.

#6about 4 minutes

Using the Isabelle proof assistant for financial logic

The Isabelle proof assistant is used to model financial operations and mathematically prove that properties like the total money supply remain constant.

#7about 3 minutes

Integrating formal verification into the development workflow

A practical approach involves prototyping new, high-risk features in Isabelle to find design flaws before committing to a full implementation in languages like Go.

#8about 2 minutes

Answering questions on writing good specifications

The discussion covers the challenges of writing complete specifications, deriving programs from them, and why even a partial specification is better than none.