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?

>>7
just because it's not perfect doesn't mean it isn't better than everything else out there.
when you've proved that the implementation conforms to the spec down to the hardware level, all you have to do is prove that the spec is correct. and mathematicians have been doing formal proofs for 200 years, so that's not a mystery.
after that, the only thing you've got left to worry about is cosmic rays flipping bits.