Yeah, that's the basic idea of refinement based program verification. An example of that is: https://github.com/seL4/l4v https://github.com/seL4/l4v There are

Yeah, that's the basic idea of refinement based program verification. An example of that is: https://github.com/seL4/l4v https://github.com/seL4/l4v There are many programs which can be nicely specified with logic, and which could thus be treated this way. That we haven't build up the infrastructure yet to do this cheaply and routinely for those kinds of programs / libraries has various reasons. For example software engineers never doing a computer science degree ;-)