Y Math? To prove and verify!

Michael Naehrig, Microsoft
-
ECE-125

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.

Event Type
Event Subcalendar