| 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. |