The past decade has witnessed a sea change in the perception of formal software verification. For instance, the microkernel seL4, whose correctness and security have been formally verified, is routinely cited to argue the improving power of verification for critical software. However, formal verification remains a long way from influencing software development practice, not least because it remains poorly integrated with programming languages.

In this talk I argue that, just as domain specific programming languages improve programmer productivity, verification can be greatly simplified by programming critical software in special purpose languages designed for verification. I present some recent work applying this idea to develop formally verified file systems code, where we developed the Cogent, a purely functional language with a self-certifying compiler to C. I will also present some early work applying these ideas to develop security-critical systems in collaboration with the Australian Government’s Defence Science and Technology Group. Here, by carefully designing the programming language to make security a first-class concern, we aim to reduce the cost of verifying system security to near-zero, while achieving unprecedented security guarantees. Finally, I draw on this collaboration to explain the surprising interplay between security verification and human factors that we are only just beginning to understand.