Proof based trusted computing. seL4 and similar applications of coq proof assistant. Existing academia is funding some development of tools like coq, and also

Proof based trusted computing. seL4 and similar applications of coq proof assistant. Existing academia is funding some development of tools like coq, and also some core applications like seL4, and more accessible applications will happen as open source. But we need to make these techniques more accessible for larger applications that will affect the real world. Example: A webserver proved to respond only to correctly authenticated clients (covering the end to end: kernel, server, protocols, for every client). Also fund making this research more accessible: try, compare, file usability bugs on, and then highlight the different technologies for achieving trust. For example Haskell Liquid types as a lighter weight complement to proving stuff in coq. Maybe fund research meshing these techniques with languages that provide different type-system guarantees, such as Rust.