Matej Penciak
Matej Penciak works with Reilabs on formal verification for zero-knowledge software. His work includes Lampe, a Lean-based tool for checking the semantic correctness of Noir programs, including challenges involving nondeterministic execution and mutable memory.