Adam Chlipala

Adam Chlipala is the Arthur J. Conner (1888) Professor of Computer Science at the Massachusetts Institute of Technology (MIT), where he is a faculty member in the Department of Electrical Engineering and Computer Science (EECS), the Computer Science and Artificial Intelligence Laboratory (CSAIL), and leads the Programming Languages & Verification Group. He has been a faculty member at MIT since 2011, following a postdoctoral position at Harvard University.

• PhD in Computer Science, UC Berkeley (2007)
• BS in Computer Science, Carnegie Mellon University (2003)

His research lies at the intersection of programming languages and formal methods, with a strong emphasis on using the Coq proof assistant to build verified compilers, cryptographic systems, and hardware-software stacks. His work spans from high-level language design to gate-level hardware verification, aiming for end-to-end correctness proofs. Recent efforts focus on high-performance parallel computing systems with full formal assurance.

The 15 most recent publications highlight a consistent trend in verified compilation, cryptographic security, hardware verification, and tensor/ML program optimization. His work increasingly integrates software and hardware verification, emphasizing modular, extensible frameworks and end-to-end correctness. Key themes include side-channel resistance, automated proof techniques, and practical deployment of formally verified systems.

• Advisory Board Member, BlueRock Systems (formerly BedRock Systems)
• Member, DARPA Information Science and Technology (ISAT) Study Group (2018–2022)
• Advisory Board Member, SiFive
• Former Advisor, krypt.co (acquired by Akamai)

Chlipala has advised numerous PhD and Master’s students and regularly teaches core MIT courses such as 6.009 (Fundamentals of Programming), 6.042 (Mathematics for Computer Science), and 6.822/6.5120 (Formal Reasoning About Programs). He is the author of the widely used textbook Certified Programming with Dependent Types and co-developer of the FRAP (Formal Reasoning About Programs) educational materials. He is also the founder of Nectry, a startup based on Ur/Web and UPO, aiming to democratize enterprise application development through AI-assisted, type-safe programming.

His research group develops tools and frameworks for modular verification, verified compilation, and formal analysis of complex digital systems. The work is deeply collaborative, involving students, industry partners, and open-source contributions via GitHub. Projects like Fiat Cryptography have been deployed in major web browsers, demonstrating real-world impact.