Adam Chlipala
Professor of Computer Science
Programming Languages & Verification Group (more PL at MIT)
Computer Science and Artificial Intelligence Laboratory
Department of Electrical Engineering and Computer Science
Office: 32-G842
Contact Information - Publications [BibTeX] - CV: HTML, PDF
Startup update: Nectry is my startup based on Ur/Web and UPO, with a "no-code" product that sets people across the business world free to build their own "enterprise-software" apps quickly, without knowing a thing about programming. It combines a tasteful component architecture in richly typed functional programming with a large-language-model AI frontend that makes "programming" like chatting with a person who is building your app while you watch. We're in the earliest stages of setting up pilots with customers, so pointers to potential enthusiastic early adopters are very welcome; and we may be able to hire more engineers soon to do work related to compilers, language design, and IDEs.

I'm interested in redeveloping the full stack of tools used by engineers to create hardware-software systems. My traditional areas are programming languages and formal methods (especially with the Coq proof assistant), but I often work on problems at the interfaces with cybersecurity, computer architecture, databases, and operating systems.

When I started as faculty, I didn't know what the heck people meant when asking about my advising style, but now I have some answers. My recruiting these days is mostly focused at the PhD level and below, though I might be persuaded to hire a postdoc with just the right match of expertise. Current MIT students (undergrad, MEng, PhD) interested in working together should e-mail me, while for others I suggest following our normal PhD application process.

For a bit more info on what I work on, two low-time-investment overviews (of the mechanized-proofs part) are my blog post on the surprising security benefits of formal proofs and video of a talk I gave at the 34th Chaos Communication Congress in December 2017.

Current Research

End-to-end hardware-software verification My main interest is in codesigning development tools and system components, across complete digital stacks (hardware and software), for delivering full systems that have unified, machine-checked correctness proofs (usually in Coq). I split my research time about evenly between software and hardware projects, which almost all involve embedding different languages and formal-methods approaches in Coq, with occasional efforts to integrate them together into demos. Our first unified demo was the verified IoT lightbulb, connecting together proofs of a RISC-V microcontroller, the compiler for the Bedrock2 low-level software language, and device drivers and application code written in Bedrock2. Our second unified demo is the verified garage-door opener, which is software-only but includes an implementation of a cryptographic protocol, where most software is generated automatically from functional programs in a variety of ways. The second demo incorporates our Fiat Cryptography project, a domain-specific verified compiler and one of the highest-impact formal-methods projects yet by number of devices that have installed software produced with it (e.g., Fiat Cryptography code ships with essentially all web browsers and mobile platforms in their TLS libraries).
End-to-end side-channel security We are also working toward proofs of timing side-channel security for full hardware-software stacks, tackling both of the main techniques: programming with constant time and using combinations of hardware and software to implement strong process isolation.
High-performance computing I'm ramping up the share of my research attention spent on high-performance computing, broadly construed, including programming with tensors and online transaction processing, with high parallel scaling. I believe multicore hardware architectures as we know them today offer both terrible programming experiences and poor performance scaling, and I'm excited about what comes next, which I'm investigating from the perspectives of both new (verified) software compiler styles and tools for rapid development of new (verified) highly concurrent hardware designs.

Some Old Research

Ur/Web, a domain-specific functional programming language for modern Web applications. I started working on it when I was a grad student, and it's pretty much done research-wise, yielding a production-quality tool suite that a fair number of people enjoy using.
Lambda Tamer, an umbrella library for the experiments in compiler verification that I started as a grad student. The most concrete outcome of the work was the parametric higher-order abstract syntax (PHOAS) encoding of program syntax, which we still put to use in many of my projects, where different kinds of compilers remain frequent ingredients in novel system designs.
FSCQ, a file system verified in Coq using a separation logic for reasoning about crash safety, mostly carried out these days by colleagues in the PDOS group
DeepSpec The Science of Deep Specification, a National Science Foundation Expedition in Computing, 2016-2021, promoting similar full-stack-verification research to what I described above, butf on more conventional architectures

Research Students




Past students


  • Spring 2024: 6.1010: Fundamentals of Programming* (also Fall 2022, Fall 2021 [as 6.009], Fall 2020 [as 6.009], Spring 2019 [as 6.009], Fall 2017 [as 6.009], Fall 2016 [as 6.009], and Fall 2015 [as 6.S04])
  • Spring 2023: 6.5120: Formal Reasoning About Programs* (also Spring 2022 [as 6.822], Spring 2021 [as 6.822], Spring 2020 [as 6.822], Spring 2018 [as 6.822], Spring 2017 [as 6.887], and Spring 2016 [as 6.887])
  • Spring 2015: 6.042: Mathematics for Computer Science (also Spring 2012)
  • Fall 2014: 6.170: Software Studio
  • Fall 2013: 6.820: Foundations of Program Analysis
  • Spring 2013: 6.033: Computer Systems Engineering [recitation instructor]
  • Fall 2012: 6.005: Software Construction
  • Fall 2011: 6.892: Interactive Computer Theorem Proving*
  • (An "*" indicates a class I [co]created.)


    Certified Programming with Dependent Types

    Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant

    An introduction to the Coq proof assistant, assuming just familiarity with rigorous math and functional programming. Presents the techniques needed to scale to large formal developments in program verification and other domains, including scripted proof automation and expressive types for embedded programs.


    Formal Reasoning About Programs

    Introducing Coq simultaneously with semantics and program proof methods. Emphasizes commonalities through casting (almost) everything in terms of invariants on transition systems, with abstraction and modularity as our standard tools for simplifying invariant proofs. Presents ideas in parallel as chapters of a PDF with standard math notation and in Coq source files, mixing in bits of proof-automation wizardry at the author's whim. [I've used this book so far in six iterations of a graduate class, and I do believe the materials are now ready to be picked up and used pretty directly elsewhere!]

    Advisory-Board Memberships

  • BedRock Systems [since 2018]: verified systems software for safety-critical computing
  • DARPA Information Science and Technology (ISAT) study group [2018-2022]
  • SiFive [since 2018]: rapid development of custom hardware solutions, based on RISC-V
  • Former

  • [2016-2019]: smarter management for cryptographic keys (acquired by Akamai)
  • How to Pronounce my Last Name

    Pretend the first "l" isn't there ("Chipala") and you'll get close enough.

    Recommended Reading

    I'm straying pretty off-topic here, but, especially for all the students who might be reading this far down the page, I'd like to recommend a few books that have had big influences on me and that I wish I'd been told about as a student.

    More content and links....