Lambda the Ultimate

People have mentioned Bedrock on and off here over the years. I found the latest paper to be an exciting read since for some strange reason I like the idea of verification.

From Network Interface to Multithreaded Web Applications:
A Case Study in Modular Program Verification.

This paper reports on one case study applying modular proof techniques in the Coq proof assistant. To our knowledge, it is the first modular verification certifying a system that combines infrastructure with an application of interest to end users. We assume a nonblocking API for managing TCP networking streams, and on top of that we work our way up to certifying multithreaded, database-backed Web applications.