Formally Verified
Philip Reiner and Peter Hayes with Adam Wick
SUMMARY
This episode of The Fourth Leg podcast features Adam Wick, Principal Scientist, Mobile Security & Systems Software for Galois, and one of the world’s leading experts on secure operating systems design and implementation. In this podcast, Wick discusses how formal methods, a precise mathematical description of a system’s function, is a crucial component to the design and implementation of CATALINK — a radically simple and secure nuclear crisis communications hotline. We dive deep further into the substance of how formal proofs not only minimize language misunderstandings in a system as complex as NC3, they provide a rigorous executable specification on how a system such as CATALINK is supposed to run.
This podcast is accompanied by Adam Wick’s paper and call to action: “Formal Methods for NC3 Systems.”