Tej Chajed

minimal-elf. Creating a minimal ELF file

iris-simp-lang. We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

coq-record-update. Library to create Coq record update functions

ltac2-tutorial. Ltac2 tutorial

database-stream-processing-theory. Formalization of DBSP

coq-tla. Coq

rdb. Debugger written in Rust

futex-tutorial. C

coq-tactical. Library of Coq proof automation

sys-verif-fa24. Course website for Systems Verification Fall 2024

rust-nbd. Network Block Device (NBD) server and client written in Rust

protocol-verification-fa2023. Assignments for COMP SCI 839 from UW-Madison in Fall 2023

audiobook-splitting. Splitting audiobooks by chapter

coq-ltac2-experiments. All the code I've ever written in Ltac2

botc-tools. Storyteller tools for Blood on the Clocktower

div-regex. Computing regular expressions to test divisibility

coq-io. Modeling I/O in Coq using free monads

goedel-t. Formalization of termination of Gödel's System T

iris-named-props. Named Props for Iris

spacemacs-coq. A Coq layer for Spacemacs

Voting.jl. Implementations of several voting schemes in Julia

sys-verif-fa25. Course website for Systems Verification Fall 2025

coq-sep-logic. Separation logic library for Coq

portmap. Map domain names to local ports with DNS and reverse proxy magic

personal-website-demo. Template for a statically generated academic website

dafny-syntax-tutorial. Short introduction to Dafny

sys-verif-fa24-proofs. Assignment repo for Systems Verification Fall 2024 at UW-Madison

coq-array. Coq library for array indexing and subslicing

dotfiles. Personal dotfiles configuration

regex-derivative. Regex derivatives in Coq

ivy-mutex. Mutex proof in Ivy

better-website. HTML

seplogic-demo. Demos for lecture on Separation Logic by O'Hearn from CACM 2019.

coq-curry-howard. What a Coq proof actually is

mailboat. Verified mail server

cardinality. Reasoning about finite type cardinality in Coq

coq-project-template. Example project setup for Coq that supports git submodule dependencies

coq-record-update-plugin. Coq

coq-transitions. Coq library for writing transition relations

split-proposal. Split an NSF proposal into submission documents

commit-email-bot. GitHub app that sends an email with every commit diff

ivy-to-mypyvy. Convert an Ivy liveness problem to a mypyvy input file

strong-induction. Proof of strong induction in Coq

madcap. A music clustering program.

python-html2rest. Convert HTML to reStructuredText

detex-abstract. Turn a LaTeX abstract into a Markdown abstract

100game. Analysis of the 100 game

wordenc. Go

specious-db. Simple persistent key-value store for prototyping a verified version

web-timer. Simple web timer