UWashington Y Math Seminar: Michael Naehrig

In mathematics, a proof not only demonstrates that a statement is true; it also allows others to confirm its correctness by verifying the argument. This talk highlights two places where the same “prove and verify” principle is applied to build trustworthy security-critical systems by producing evidence that others can independently verify. First, we look at end-to-end verifiable elections, where cryptographic techniques ensure ballots are well-formed and tallying is correct while preserving voter privacy. Second, we discuss formal verification of cryptographic software in Lean, linking implementations to precise specifications and even validating the specifications themselves.