seL4 formally verified microkernel

https://sel4.systems/

This is the kernel that flies the X-37 Orbital Test Vehicle. Why aren't you using it in your embedded programming?

Anyway, this got me thinking about formal verification. Is it overrated crap to suck out more research grant money, or is it worthwhile to learn and apply?

Does it make unit-testing look like something retarded drooling code-monkeys do?

It seems difficult to use in the real world. Can it be made simpler? What if everything was written with formal proofs?

Are dynamically typed languages impossible to automatically verify?

>>6
oh, I agree that formal verification can be useful (although the way it is done now means it's usually more hassle than it's worth). it's just that it isn't a silver bullet that will magically make everything bug-free and secure because it still requires correct specification (a big thing - there are plenty of serious bugs made at the design stage, and they often impact security) and correct assumptions (also a big thing - people won't always use your software the way you imagine them using it).