Verification for mortals

An open secret about formal verification is we've known how to do it since 1967.

On pen and paper, that is.

It's been nearly 60 years and no one has built a practical system for verifying software.

The verifiers that do exist require a team of PhDs to operate, or are so limited they can't be used for real software (no I/O support, for example).

Emphasis has also fallen on getting the machines to deduce properties, a blind alley, rather than on adapting pen and paper arguments for verifiers.

We think the industry optimised for the wrong thing.

Programmers already build kernels that run the world's infrastructure, compilers, cryptographic protocols, and distributed systems trusted by billions.

Mathematicians already prove theorems that enable us to split atoms, put satellites in space, and settle centuries-old conjectures.

The missing ingredient in formal verification is not reasoning, but effective tools for expressing reasoning to machines.

Verification does not become practical by machines replacing human understanding.

It becomes practical when formal systems fit naturally into the way we think. In other words:

Verification is a user interface problem.

Xr0

Xr0 is a verifier for C.

Most verification systems force programmers outside their region of expertise, and into the specialised jargon of traditional mathematics.

Xr0 inverts this. Verification is just programming, and this is how it feels in Xr0.

Programmers already know why their code works: Xr0 just makes it easy for them to show this.

It focuses on eliminating all memory unsafety problems from C, because this is the hardest and most important challenge in systems software today.

After finishing with the safety problem, we will turn our attention to verification of arbitrary desired properties. See more → xr0.dev.

i2

i2 is a language for mathematical reasoning.

Proofs in most proof assistants do not at all resemble pen and paper proofs, and the mapping between the two is very unclear, making the learning process very difficult.

Thus, despite computers being everywhere in science, proofs in mathematics are still done on paper.

Instead of focusing on research mathematicians at the frontier of their field (a worthy pursuit handled by projects like Lean), i2 attempts to provide an interface that is accessible to high school students and undergraduates.

i2 uses a calculational proof style developed by W.H.J. Feijen and Edsger Dijkstra, which is relatively easy to use both on pen and paper and formally on a computer. See more → i2lang.org.