About Me
My name is Matej Penciak. I am a research scientist at the Beneficial AI Foundation where I am working on Aeneas, a tool to reason about Rust. In my previous roles I was worked on formal verification of smart contract languages and zero knowledge protocols.
At Reilabs I worked on lampe, a tool to reason about the functional correctness of programs written in Noir. At Argument Computer Company I worked on the cryptography of the Lurk ZKVM.
Throughout all my experience as a professional software engineer, my main programming language and tool has been Lean. I am particularly proficient in tactics and metaprogramming.
Before this I was a research mathematician interested in algebraic geometry, and integrable systems. I still like to dabble in the field, so check out some of my math projects to figure out what I'm thinking about.
I am proficient in Lean, Rust, and Python. I am currently working on a simple compiler written in Lean. Check out the progress here
Check out my up to date resume and CV for all the boring stuff.