Three talks at the recent #ZKProof 7 conference in Sofia caught our attention:
🔹 Alexander Hicks from Ethereum Foundation had some really nice things to say about #LeanLang, calling it "quite a nice functional programming language". 😍 He showed off zkLib, which ties executable implementations of proof systems directly to security proofs.
https://www.youtube.com/live/L_uz5rH50Sw
🔹 James Parker from Galois introduced zkLean - a DSL for specifying ZK statements in Lean. Definitely worth checking out if you're interested in this space!
https://www.youtube.com/live/O_bT89JK6_c
🔹 Jonathan Rouach from QEDIT discussed the motivation behind the development of a Lean end-to-end proof of the PLONK verifier.
https://www.youtube.com/live/dNLa5B2ER74