François Garillot

François Garillot

Research engineer and coffee fan.

Talks and presentations (selected)

Lurk: Lambda, the Ultimate Recursive Knowledge

September 07, 2023

Talk, ICFP 2023, Seattle, WA, USA

We introduce Lurk, a new LISP-based programming language for zk-SNARKs. Traditional approaches to programming over zero-knowledge proofs require compiling the desired computation into a flat circuit, imposing serious constraints on the size and complexity of computations that can be achieved in practice. Lurk programs are instead provided as data to the universal Lurk interpreter circuit, allowing the resulting language to be Turing-complete without compromising the size of the resulting proof artifacts. Our work describes the design and theory behind Lurk, along with detailing how its implementation of content addressing can be used to sidestep many of the usual concerns of programming zero-knowledge proofs.

Nova ZK Proof Verification in the EVM

August 26, 2023

Talk, Rust x Ethereum Day, San Francisco, CA, USA

We introduce the challenges of writing a verifier for the Nova ZKP system on Ethereum, and the methods used to overcome those challenges.

Lambda the Ultimate Recursive Knowledge

April 04, 2023

Talk, ZKSummit 9, Lisbon, Portugal

We introduce Lurk, a groundbreaking LISP-based programming language for zk-SNARKs. Unlike conventional approaches that involve compiling computations into flat circuits, Lurk allows programs to be provided as data to the universal Lurk interpreter circuit. This innovative design empowers Lurk with Turing-completeness, without sacrificing the size of the resulting proof artifacts.

Taming the Many EddSAs

March 08, 2023

Talk, NIST Crypto Reading CLub, Virtual

In this talk we will discuss the security of concrete instantiations of EdDSA by identifying exploitable inconsistencies between standardization recommendations and Ed25519 implementations. We will mainly focus on current ambiguity regarding signature verification equations, binding and malleability guarantees, and incompatibilities between randomized batch and single verification. Based on our work that appeared at SSR 2020, we will give a formulation of the Ed25519 signature scheme that achieves the highest level of security, explaining how each step of the algorithm links with the formal security properties.

Mechanized Proof for the Libra Blockchain

May 27, 2020

Talk, TPBC Weekly seminar series, Barcelona, Spain

This talk presents formal methods work on the Diem (formerly Libra) blockchain, including a formalization of the safety of consensus in Coq.