About the effort being worth it or not, I believe that security critical programs MUST have formal proofs. Vulnerabilities in this kind of software are extremely costly. The same goes for software whose failure can be of danger for humans (c.f. the Toyota debacle).
If you can have a tiny trust-kernel that has been proof-checked, keep everything else outside of it, and the things outside of it can only communicate with (or even observe) their peers via messages sent through it, then you don't need to worry about including untrusted code in your app.
Instead, you just slap any and all untrusted code into microservices (microdaemons?) in their own security domains/sandboxes/VMs/whatever, and speak to them over the kernel's message bus (or in the VM case, a virtual network), and suddenly they can't hurt you any more.
https://www.schneier.com/blog/archives/2015/05/friday_squid_...
That's a serious issue that's killed a number of past projects. At least many modern ones learned the lesson and are acting accordingly.
But yes, it is remarkable how far things have come with regards to formal methods. But it is still quite tedious to do unless you're an academic working in the field.