Stavan Jain

First-year Computer Science PhD student at UW–Madison

My research focuses on the formal verification of quantum error correcting codes using the Lean proof assistant. The properties these codes are claimed to have, such as distance, are often established by a solver or an informal argument rather than a proof, leaving the people who build compilers and architectures to take them on trust. My goal is to develop QECLean, a comprehensive formalized library for the theory of quantum error correction and a trusted base of knowledge the field can build on.

Once the theory is formalized, those properties become machine-checkable, which opens the door to searching for new codes rather than hand-designing them. I am building an LLM-driven pipeline that proposes and verifies candidates against QECLean, optimizing for both encoding rate and code distance. Every code it finds is physically realizable and has a formalized proof of its parameters.

I am advised by Aws Albarghouthi and I'm involved with the madPL and Quantum Computing groups at UW–Madison. I earned a B.S. in Math and Computer Science at Duke University, where I worked with Professor Colleen Robles .

See projects or get in touch.