Time: Thursday April 11th, from 4:45pm to 6pm
When you program SNARKs, you write a program that generates a constraint system that you hope enforces some high-level property that you have in mind. But how do you know for sure that the constraint system you wrote down does indeed enforce that property? There is an almost exactly analogous problem which occurs in programming in general: how does one know that the program one has written conforms to a particular specification?
Formal verification (FV) refers to a set of techniques for writing formal proofs of adherence of a program to a specification. FV is still a highly specialized skill, and can reasonably handle only moderately complex protocols and code, but interest in these techniques is growing substantially. Today, commercial and government organizations actively employ FV on critical areas of protocols, and aim to expand that coverage to formally verify entire protocol libraries.
In this breakout session, we introduce the basic notions of FV. We then lead an exploratory discussion to identify the diverse abstractions that may be useful in formally proving correctness of SNARK programs.
See you there!
David and Izaak