Tej Chajed
I'm Tej Chajed, and I'm a Research Scientist at Theorem. I work on using AI to enable formal verification at scale.
I was an assistant professor in Computer Science at the University of Wisconsin–Madison for three years before I moved to industry. Prior to that I did a one-year postdoc at VMware Research, and before that I got my PhD from MIT in the PDOS group.
Research
I helped develop Perennial and Goose, a system for verifying Go code that supports concurrency and distributed systems. I do a lot of work on Rocq things, including maintaining a list of Rocq tricks for the advanced user and contributing to Iris.
I'm passionate about teaching and technical communication. I was a Fellow in MTLE at UW–Madison, where I learned a great deal about effective teaching. During my PhD, I was a communication Fellow in the EECS Communication Lab, where I helped students with technical communication.
Selected publications
All papers
Software
- perenniala system for verifying Go programs with concurrency
- iris-simp-langinstantiating Iris for a simple programming language
- botc-toolsstoryteller tools for running Blood on the Clocktower
Teaching
- Spring 2026 — CS 537, Operating systems
- Fall 2025 — CS 839, Systems verification
- Spring 2025 — Teaching release
- Fall 2024 — CS 839, Systems verification
- Spring 2024 — CS 537, Operating systems
- Fall 2023 — CS 839, Protocol verification
As a graduate student I helped create 6.826 (Principles of Computer Systems) at MIT, where I built the lab assignments and TA'd in Fall 2020, Fall 2019, and Fall 2017.
