Rust предотвращает многие ошибки работы с памятью, но программа всё ещё может вернуть неверный результат. Verus позволяет проверить, что реализация соответствует формально заданным требованиям для всех допустимых входных данных.
Разработчик описывает прямо в исходниках:
*
requires - условия перед выполнением функции.*
ensures — свойства результата.* Инварианты циклов и вспомогательные доказательства.
Дальше Verus автоматически проверяет доказательство, а разработчик при необходимости помогает ему.
В статье есть показательный пример с бинарным поиском. Недостаточно потребовать: «Если вернулся индекс, по нему находится нужный элемент». Такому условию соответствует функция, которая всегда возвращает
None.Нужно добавить второе требование: если вернулся `None`, искомого элемента действительно нет в массиве.
Amazon уже использует Verus для проверки ключевых примитивов Nitro Isolation Engine, отвечающего за изоляцию виртуальных машин. Инструмент также позволяет доказывать свойства конкурентного кода и безопасность поддерживаемых конструкций
unsafe.Гарантии относятся к заданной спецификации и принятым допущениям: полнота самих требований остаётся ответственностью разработчика.
📖 https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus
#Rust #Разработка #FormalVerification
