верифай, но проверяй
This paper thoroughly analyzes three state-of-the-art, formally verified implementations of distributed systems: IronFleet (Dafny/C#), Verdi (Coq/OCaml), and Chapar (Coq/OCaml). Through code review and testing, we found a total of 16 bugs, many of which produce serious consequences, including crashing servers, returning incorrect results to clients, and invalidating verification guarantees.
https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf
В протоколах и их доказанных реализациях багов не нашли, все баги были на границе взаимодействия верифицированного кода с жестоким внешним миром - неверифицированным окружением. Сложно описать формально все возможные косяки низкоуровневых библиотек и сторонних процессов. Смешной момент - Dafny для верификации использует Z3 солвер, если солвер невовремя прервать, Дафни считает, что все ок и считает недопроверенную программу годной.
А тут мужики нагенерили много тестовых программок для компиляторов:
In less than six months, our approach has led to 217 confirmed GCC/Clang bug reports, 119 of which have already been fixed ... In about three weeks, we have also found 29 CompCert crashing bugs, and 42 bugs in the production Scala compiler and the Dotty research compiler.
https://arxiv.org/pdf/1610.03148.pdf
GCC и Clang могут падать, а могут неправильный код генерить. CompCert (который на Coq'e верифицирован), как я понял, неправильный код не генерит, но вот сам падать может - ассерты срабатывают внутри, т.е. некоторая неконсистентность логическая там была.
https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf
В протоколах и их доказанных реализациях багов не нашли, все баги были на границе взаимодействия верифицированного кода с жестоким внешним миром - неверифицированным окружением. Сложно описать формально все возможные косяки низкоуровневых библиотек и сторонних процессов. Смешной момент - Dafny для верификации использует Z3 солвер, если солвер невовремя прервать, Дафни считает, что все ок и считает недопроверенную программу годной.
А тут мужики нагенерили много тестовых программок для компиляторов:
In less than six months, our approach has led to 217 confirmed GCC/Clang bug reports, 119 of which have already been fixed ... In about three weeks, we have also found 29 CompCert crashing bugs, and 42 bugs in the production Scala compiler and the Dotty research compiler.
https://arxiv.org/pdf/1610.03148.pdf
GCC и Clang могут падать, а могут неправильный код генерить. CompCert (который на Coq'e верифицирован), как я понял, неправильный код не генерит, но вот сам падать может - ассерты срабатывают внутри, т.е. некоторая неконсистентность логическая там была.