It has become apparent that producing systems software to the highest degree of assurance is possible, without sacrificing performance, and at lower cost than has historically been assumed. With careful design and effective use of automation, it should be possible to reduce the cost to the point that such an approach is commonplace for critical systems, and tackle currently unsolved issues, including concurrency. A strong familiarity with the discipline of low-level systems programming, and an understanding of the application domain will remain essential to ensure that performance is not sacrificed. Likewise, a clear understanding of the state of the art in formal verification is essential to ensure that systems are designed such that verification remains tractable.