Verifying Proofs on Blockchain

In cryptography, a *proof system* is a protocol between a prover and a verifier that enables the prover to convince the verifier that a claim is true. They are often probabilistic; given a source of randomness, it is often more efficient to convince the verifier only that it is very likely that the claim is true. Such proof systems now have interesting applications to blockchain technology, where they are used, among other things, to validate the execution of smart contracts.
It is easy to make mistakes when implementing cryptographic protocols and designing smart contracts, and billions of dollars are lost to hacks every year. Fortunately, another proof technology can help: interactive proof assistants, which have long been used to verify hardware and software systems, can also be used to verify the correctness of cryptographic protocols.
In this talk, I will describe some formal verification efforts I have carried out with colleagues at StarkWare Industries using the Lean proof assistant. I will explain some of the ideas behind smart contracts and interactive proof assistants without assuming familiarity with either.