NASA software is very good, but not in general formally verified, I think (based mostly on reading postmortems on various NASA failures). Even TLA+ analysis an

NASA software is very good, but not in general formally verified, I think (based mostly on reading postmortems on various NASA failures). Even TLA+ analysis and proof of correctness doesn't stop things like "new zookeeper clients are pushing a lot of new writes => disk space needed for logs increases => across all the nodes in the zookeeper cluster => the entire formally correct cluster keeps falling over now but it didn't last week" I meant more in the sense of the proofs in TAOCP - these are programs that don't interact with anything outside of the program itself, no non-specified input, so a lot simpler, no dates, no actual machine memory, just a little synthetic world defined by the language itself. Even TeX is imagined to be unchanging after Knuth's passing, and is basically unchanged since the 70s. For sure the world has moved on, but we have lost the ability to have confidence in the software and have had to develop tools and ways of thinking inspired by biology.