Исследователи разработали конвейер верификации, который автоматически преобразует криптографический код Rust в машинные доказательства в Lean 4. Сочетая инструменты символьного извлечения с ИИ-проверами, эта система успешно подтверждает корректность сложных примитивов, гарантируя надежность через проверку на уровне ядра.