Joonwon Choi


I'm a graduate student at MIT CSAIL, currently co-advised by Adam Chlipala and Arvind. I'm interested in formal verification for any computer systems that are hard to believe to be correct. I'm an advocate of mechanized proofs, I like to prove something with Coq. I don't believe things not proven.

Office : 32-G888, Stata Center, 32 Vassar St, Cambridge, MA 02139

Email : | Phone : +1-339-225-5940

Research Interests

My current research interests are as follows:

  • Kami: formal verification for correct hardware design and synthesis, based on modular proof.
  • Hemiola: structural design and proof of hierarchical cache-coherence protocols, based on serializability guarantee in message-passing systems.
  • The end-to-end proof between hardware and software.



  • Kami: A Platform for High-Level Parametric Hardware Specification and its Modular Verification. [pdf]
    Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind.
    Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP'17). September 2017.
  • An Inlining Approach to Formal Hardware Semantics. [pdf]
    M.S. Thesis in Electrical Engineering and Computer Science, Massachusetts Institute of Technology.
  • Crellvm: Verified Credible Compilation for LLVM [pdf]
    Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, and Kwangkeun Yi.
    Proceedings of the ACM SIGPLAN 2018 Conference on Programming Language Design and Implementation (PLDI'18). June 2018.
  • EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. [draft]
    Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, C├ędric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Beguelin.
    To appear in IEEE Symposium on Security and Privacy (Oakland), May 2020.

Awards and Honors

  • Sep 2014 - Current, Kwanjeong Educational Fellowship
  • Sep 2014 - Current, MIT Emerson Scholarship for Private Music Study
  • Feb 2013, Top Honor (summa cum laude) Certification
  • Mar 2006 - Feb 2013, Presidential Science Scholarship

Teaching Experience

Work Experience

  • Jul 2018 - Sep 2018, Research Intern, Microsoft Research Cambridge
  • Apr 2009 - Oct 2011, Software Engineer, allm Games (Skilled Industry Personnel)
  • Jan 2009 - Apr 2009, Software Engineering Intern(SWE), Google Korea
  • Jul 2007 - Aug 2007, Intern, SK Communications