@ilyasergey
Формальные методы достигли важного этапа: теперь они способны массово верифицировать реальные бинарные файлы. Однако масштабированию мешают спецификации с единственной точкой входа, огромные доказательства и слабое повторное использование. Решением автор считает композиционное рассуждение и модульные абстракции.