I lead a research collective known as VIP, named after Verification and Intelligence for Programs. Our work sits at the intersection of formal verification--employing rigorous mathematical methodologies to ensure the reliability of safety-critical systems--and code intelligence, which leverages Large Language Models to automate the understanding, generation, analysis and optimization of programs. Beyond general-purpose programming, we specialize in the security and correctness of zero-knowledge proof circuit programming and cryptographic systems like zkVMs.

Furthermore, we actively seek candidates with an interest in theoretical computer science and AI for sciences.