Tej Chajed

chajed@wisc.edu
Computer Sciences 7361

I'm Tej Chajed, an assistant professor in Computer Science at the University of Wisconsin-Madison. I work on formal verification of systems software — I implement systems and prove they do what they're supposed to.

Prior to joining UW-Madison I did a one-year postdoc at VMware Research, and before that I got my PhD from MIT in the PDOS group.

I'm actively looking for new students! If you're interested in working with me please set up a time to chat about potential projects.

Research

Even critical systems software has bugs — for example, file systems have bugs that occasionally lead to users losing data. My research aims to write systems software that always does what it's supposed to. We do this with formal verification: we write a precise specification of what the system is supposed to do and prove that the implementation meets the specification. My research has culminated in DaisyNFS, a verified, concurrent file system that gets good performance. The path to verifying DaisyNFS involved developing new frameworks and tools, including Perennial, a framework for reasoning about crash safety and concurrency, and Goose, a system for connecting the proofs to Go code.

I do a lot of work on Coq-related things, including maintaining a list of Coq tricks for the advanced user and contributing to Iris.

During my PhD, I was a communication Fellow in the EECS Communication Lab, where I helped students with technical communication. I'm still passionate about helping people with writing and presenting, so please reach out if you think I could help with something!

Teaching

CS 839: Systems verification (Fall 2025)

Teaching release (Spring 2025)

CS 839: Systems verification (Fall 2024)

CS 537: Operating systems (Spring 2024)

CS 839: Protocol verification (Fall 2023)

As a graduate student, I helped create 6.826 (Principles of Computer Systems), a class on systems verification, and in particular I created the lab assignments. I was a TA for the class in Fall 2020, Fall 2019, and Fall 2017.

Publications

Verus: A Practical Foundation for Systems Verification (SOSP 2024)

Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno

Shadow Filesystems: Recovering from Filesystem Runtime Errors via Robust Alternative Execution (HotStorage 2024)

Jing Liu, Xiangpeng Hao, Andrea Arpaci-Dusseau, Remzi Arpaci-Dusseau, and Tej Chajed

Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas (CAV 2024)

Eden Frenkel, Tej Chajed, Oded Padon, and Sharon Shoham

Anvil: Verifying Liveness of Cluster Management Controllers (OSDI 2024)

Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu

Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs (OSDI 2024)

Tony Nuda Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, and Bryan Parno

Beyond isolation: OS verification as a foundation for correct applications (HotOS 2023)

Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, and Andrea Lattuada

DBSP: Automatic Incremental View Maintenance for Rich Query Languages (VLDB 2023)

Mihai Budiu, Tej Chajed, Frank McSherry, Leonid Ryzhyk, and Val Tannen

Verifying a concurrent, crash-safe file system with sequential reasoning (Ph.D. Thesis, MIT, 2022)

Tej Chajed

Verifying the DaisyNFS concurrent and crash-safe file system
with sequential reasoning (OSDI 2022)

Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich

GoJournal: a verified, concurrent, crash-safe journaling system (OSDI 2021)

Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich

Record Updates in Coq (CoqPL 2021)

Tej Chajed

Verifying concurrent Go code in Coq with Goose (CoqPL 2020)

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich

Verifying concurrent, crash-safe systems with Perennial (SOSP 2019)

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich

EverParse: Verified Secure Zero-Copy Parsers for
Authenticated Message Formats (USENIX Security 2019)

Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko

Argosy: Verifying Layered Storage Systems with Recovery Refinement (PLDI 2019)

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich

Verifying concurrent software using movers in CSPEC (OSDI 2018)

Tej Chajed, M. Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich

Proving confidentiality in a file system using DiskSec (OSDI 2018)

Atalay İleri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Verifying a high-performance crash-safe file system
using a tree specification (SOSP 2017)

Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Extending a verified file system with concurrency (SOSP 2017 SRC)

Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Certifying a file system using Crash Hoare Logic:
Correctness in the presence of crashes (CACM 2017)

Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, and Daniel Ziegler

Using Crash Hoare Logic for certifying the FSCQ file system (SOSP 2015)

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

Amber: Decoupling user data from web applications (HotOS 2015)

Tej Chajed, Jon Gjengset, Jelle van den Hooff, M. Frans Kaashoek, James Mickens, Robert Morris, and Nickolai Zeldovich

Service

How to pronounce my name

"Tej" rhymes with "page", and Chajed is pronounced as written (CHA-jed).