types: simple
logic: higher-order
proof: machine-checked
software: formally verified

        Atom Feed

Gerwin's Style Guide for Isabelle/HOL. Part 2: Good Style.

The dos and don’ts of Isabelle proofs - Part 2: Good Style. Advanced material for nicer proofs.

With examples and rationale.

Read more »

Isabelle Style Part 2

Isabelle Style

Gerwin's Style Guide for Isabelle/HOL. Part 1: Good Proofs.

The dos and don’ts of Isabelle proofs: guidelines for making your proofs more readable, maintainable and enjoyable.

With examples and rationale.

Read more »

So you want to be a proof engineer?

I want to verify software!

Will prove theorems for money!

What do I need to learn?

You’re a programmer, maybe with a computer science or math degree. You’re interested in program verification and proofs, but have no previous experience in these. You want to learn. Here’s what you should read.

Read more »


Syntax Highlighting

Isabelle Syntax Highlighting in Markdown and HTML

Wouldn’t it be nice to just include snippets of Isabelle code in markdown or html and have them show up rendered with symbols and highlighting?

For instance on a blog? Or a list like the Top 100 theorems? Or on github?

Set your quick_and_dirty flags and read on.

Read more »

Mauna Kea Observatory


The craft, art, and science of interactive machine-checked proof.

This is a blog about formal software verification in general and a tendency towards interactive theorem proving and the prover Isabelle/HOL in particular.

Interactive theorem proving means constructing mathematical proofs where the computer assists in finding the proof and at the same time checks it for correctness. Proof is exciting for software verification, because you can use it as strong evidence for code correctness and for gaining high assurance in security and safety. Interactive proof is one of the most successful methods so far in applying these techniques to real software. It has the potential to fundamentally change how we build and trust critical software.

Formal proof may sound hard, but it is a skill that can be learned. It's turning from art and science into craft.





Gerwin Klein is a researcher at NICTA in computer science and formal software verification. He is teaching at UNSW, Australia, and is applying formal proofs in real-world operating system verification and programming language semantics.