Principal Investigator Adam Chlipala
A platform for building software with strong security guarantees, via machine-checked mathematical proofs about assembly code; current focuses include deriving a correct and high-performance DNS server from a specification.