Virtual Library

Our virtual library is an online repository of all of the reports, papers, and briefings that IST has produced, as well as works that have influenced our thinking.

Submit your Content

Reports

Unlocking U.S. Technological Competitiveness: Proposing Solutions to Public-Private Misalignments

Ben Purser, Pavneet Singh

viewpdf

Articles

The Phone-a-Friend Option: Use Cases for a U.S.-U.K.-French Crisis Communication Channel

Daniil Zhukov

viewpdf

Articles

China: Nuclear Crisis Communications and Risk Reduction

Dr. Tong Zhao

viewpdf

Articles

Use-Cases of Resilient Nuclear Crisis Communications: A View from Russia

Dmitry Stefanovich

viewpdf

Articles

Pakistan: Mitigating Nuclear Risks Through Crisis Communications

Dr. Rabia Akhtar

viewpdf

Articles

Resilient Nuclear Crisis Communications: India’s Experience

Dr. Manpreet Sethi

viewpdf

Reports

A Lifecycle Approach to AI Risk Reduction: Tackling the Risk of Malicious Use Amid Implications of Openness

Louie Kangeter

viewpdf

Contribute to our Library!

We also welcome additional suggestions from readers, and will consider adding further resources as so much of our work has come through crowd-sourced collaboration already. If, for any chance you are an author whose work is listed here and you do not wish it to be listed in our repository, please, let us know.

SUBMIT CONTENT

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.”

download pdf