Verve is a research operating system developed by Microsoft Research. Verve is verified end-to-end for type safety and memory safety.Because of their complexity, a holy grail of software verification has been to verify properties of operating systems. Operating systems are usually written in low-level languages, such as C, that provide very few guarantees. The Singularity project took the approach of writing an operating system in C#, a type-safe, memory-safe language.