Recently graduated Harry King just won the (university-wide) best bachelor thesis award for his thesis on “Development Tools &
Techniques for a More Robust Operating System”. For his thesis project he built an operating system kernel from scratch in Ada. The implementation in Ada allowed him to formally verify the OS components.