Thanks for the information, it is very much appreciated. I was a little frustrated that comments on this thread had people saying you should learn the math and prove your programs but providing no information on how to do so. It would be great if provided resources to show people how to do it. Or even better, provide a project that they worked on and show how they used formal methods to move through the project in detail, which would be wonderful. If someone wants to promote formal methods, then should not just argue for it, but teach it, even a tiny bit. That would get a way better reception.

A little off topic, but it would be great if there was a method/system which could provide requirements tracking down the set of artifacts to where you could point to a bit of source code and say it implements that certain requirement. Sort of like a chain of responsibility for code and associated documents. That might be a pipe dream, I don't know.

Anyway, thanks for the information, I remember seL4 being mentioned in discussion of the sorry state of software on medical devices, but had forgotten it until you mentioned it. Thanks.