Дослідники розробили конвеєр верифікації, який автоматично перетворює криптографічний код Rust на машинно-перевірені докази в Lean 4. Поєднуючи інструменти символьної екстракції зі штучним інтелектом, ця система успішно перевіряє складні примітиви, забезпечуючи надійність завдяки перевірці на рівні ядра.