Also quite famously: http://www.flownet.com/gat/jpl-lisp.html
They used a subset of C (no malloc...) and had a safety certified compiler. If you crash two trains because of a compiler bug at least you can pass the bunk. They did not use formal proof methods.
The documentation was massive, substantially longer than the code, to the extent that doing the actual implementation from the documentation seemed relatively trivial. Writing and analyzing the documentation on the other hand... I had the impression that writing documentation to that level of detail must have taken substantially longer than implementing it directly in code. And this was probably a good thing as it forced people to think more about every details.
Once a system was written it had to be certified. Any changes, no matter how trivial, meant you had to go through the whole certification process again: slow, painful and expensive.
Tools like Alloy[1] allow you to write your documentation/definition and check its consistency. These languages are always limited so you don't get into Gödel incompleteness problems.
Ada is used in the realtime life critical stuff because of the huge ecosystem from tools to paperwork behind it supporting safety. I could use C I suppose, but I simply am not smart enough to not miss a pointer dereference now and then.
It comes down to it that lisp doesn't have the ecosystem behind it for life-crtical applications. I doubt it ever will.
What it is useful for though is analysis tools - helping keep people out of those life endangering situations.
1. See Diamond da-42 takeoff crashes.