Формальной верификации обзорчик: безопасная разработка за пределами рандомизированных тестов

Что поделать, чтобы писать безопасный софт помимо code review и серьезнейшего тестирования? Писать меньше кода и больше теорем! Посмотрим, как HTTPS сейчас защищают на уровне реализации. 

Все знают, что понять код, который не влезает в один экран сложно. Какое решение? Ограничить семантику для лучшей композиции; дать пользователям волшебство дешевого моделирования; выкрутить статический и динамический анализ до 11. 

Этот доклад — ураганный пробег по стэйт-оф-зэ-арт в формальной верификации, с кейсами верифицированной ОС (CertiKOS), HTTPS-компонентов, на которых работает большая часть веб (Project Everest), и ядра Linux (linux.git/*.tla; модели блокировок). Зачем? Чтобы мы писали лучший код, разумеется. С благодатию Computer Science.