In a past life, I pushed hard for more investment in seL4 for certain defense applications. The nuance isn't to be underestimated though – I can say from experience that it's often a hard sell to folks that aren't already versed in the ins and outs of formal methods, security, kernels/operating systems, etc. There are plenty of lower hanging fruit (like networking hardware) than the applications I worked on, yet commercial adoption still seems low. Maybe this is due to that nuance. To the credit of the folks at Trustworthy Systems and UNSW, they've done a great job producing literature that outlines the business case in a manner palatable to decision makers. This paper [0] in particular came in handy to me many times.

[0] https://ts.data61.csiro.au/publications/csiro_full_text/Klei...