Fwd: [security-lunch] Feb 18 | Elizaveta Pertseva on "Automating Verification of ZKP Arithmetizations in Lean"

[Alan Karp]

--------------
Alan Karp

---------- Forwarded message ---------
From: Michael Leo Paper via security-lunch <securit...@lists.stanford.edu>
Date: Mon, Feb 16, 2026 at 6:56 PM
Subject: [security-lunch] Feb 18 | Elizaveta Pertseva on "Automating Verification of ZKP Arithmetizations in Lean"
To: securit...@lists.stanford.edu <securit...@lists.stanford.edu>

Security Lunch ⛄ Ed. — Wednesday,  Feb 18th, 2026, 12:00 pm @ CoDa E160

Automating Verification of ZKP Arithmetizations in Lean

Elizaveta Pertseva

Can't make it in person? Join us on zoom.

See our past & upcoming events on our website! 

Abstract: 

Many modern Zero-Knowledge Proof (ZKP) systems rely on arithmetizations to encode machine level (bitvector) arithmetic as finite field operations. The correctness of these arithmetizations is crucial for soundness, but constructing them can be error-prone. Existing verification workflows are either manual, requiring substantial human effort, or rely on SMT solvers, which scale poorly on these problems. In this talk, I will discuss existing verification tools and present our novel automated Lean-based approach that uses type translation to enable more scalable and trustworthy verification of ZKP arithmetizations.

Bio:

Elizaveta Pertseva is a 3rd year PhD at Stanford advised by Clark Barrett. Her research focuses on automatically formally verifying cryptographic primitives.

_______________________________________________
security-lunch mailing list
securit...@lists.stanford.edu
https://mailman.stanford.edu/mailman/listinfo/security-lunch