Три года формальной верификации алгоритмов с помощью всё более мощного ИИ

Автор делится трёхлетним опытом использования формальной валидации для алгоритмов. В 2023 году он вручную писал код на Rust и проверял его в Dafny, в 2024-м — использовал ИИ для написания доказательств в Lean, а в 2025-м ИИ уже сам пишет и реализацию на Rust, и доказательства. Теперь сложные доказательства занимают минуты, но проблема доверия к ИИ-коду остаётся нерешённой.