AWS очень большая и сложная система. Я совершенно не удивлен в том что ребята настолько активно применяют формальные методы. Ну как иначе то делать и продавать 999999999? 😎

Скорее меня удивило встретить эту статью среди прочего низкосортного в одной рассылке:
https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/

Там про то, как TLA+ оказался когнитивно слишком тяжелым, и AWS сделали свой язык P (у меня как то были знакомые которые на серьезных щах верили в то что под капотом весь AWS только на Питоне, Си и баше написан). Интересно что P теперь помогает не только на этапе просто дизайна спек, но и в продакшене через PObserve - они сгребают логи систем и проверяют что они соответствуют спекам!

И еще очень круто про continuous подход в фаззинг и хаос тестировании. При том последнее довольно агрессивное, сильнее чем я думал. Кроме того что AWS сам себя постоянно пытается сломать, у них есть Fault Injection Service который позволяет нам как клиентам в свою инфру запускать разных агрессивных обезьян 🤬

Радует еще то что отдельно говорят о том что грустно это – низкая популярность формальных методов в индустрии из за сложности в понимании / обучению, но тут есть большие надежды на AI. Пока, правда, только надежды.

В статье больше подробностей в приближении и примеров, читайте!​​​​​​​​​​​