Large commercial organizations have good reason to take the correctness of their cryptography seriously. The largest even employ “cryptography wizards”, experts in the field who are qualified to roll their own heavily optimized implementations. As skilled as these experts are, their work rarely comes with a formal, mathematical proof of implementation correctness.

I’ll discuss Google’s interest in formally verified implementations of cryptography and our experiences with an internship that focused on ECC curve P256. This project successfully verified modular arithmetic on the curve down to the specific machine representation – the register level – for an idealized bignum processor known as “Fancy Machine”.

We were able to use this experience with a different type of expert, one skilled in the art of formal verification, to build greater certainty in a prior implementation of the same curve. This is the story of the cryptography experts who told us what to prove and the formal verification experts who told us how to go about doing so.