Current projects
| Jitterbug | A framework for writing and verifying just-in-time compilers. |
| Rosette | A programming language for building verification and synthesis tools. |
| Serval | A framework for writing automated verifiers for low-level systems code. |
| SymPro | A profiler for identifying and diagnosing performance bottlenecks in programs under symbolic evaluation. |
Past projects
| Ferrite | A framework for developing file system crash-consistency models. |
| Hyperkernel | A push-button approach to building provably correct OS kernels. |
| MemSynth | A language and tool for verifying, synthesizing, and disambiguating memory consistency models. |
| Neutrons | A verifier for a subset of EPICS. Currently in use at the University of Washington Clinical Neutron Therapy System. |
| Nickel | A framework for designing and verifying information flow control systems using noninterference. |
| Synapse | A framework for specifying and solving optimal synthesis problems. |
| Yggdrasil | A toolkit for writing file systems with push-button verification. |