Nic Schleicher
Nic Schleicher works on formal verification and proof systems for post-quantum Ethereum. He is an author of leanerVM, a Lean 4 implementation and formalization of leanVM, the minimal hash-based zkVM for post-quantum signature aggregation, and contributed formally verified binary-field arithmetic to the CompPoly Lean library. He has also built STARK-provable verification and aggregation of SPHINCS+ and Falcon signatures.