DeFi· ★★★· нейтрально· 28 сентября, 20:00

CertiK формально верифицировала zkWasm с доказательствами на Coq

—Доказательства на Coq подтверждают soundness и knowledge soundness схем zkWasm
—Внутренний код проекта — около 33 000 строк Coq, из них примерно 21 000 доказательств
—Найдены два бага: пропущенное ограничение на memory load и на инструкцию Return
—Вне охвата остались Rust-код таблиц, интерпретатор Wasmi и сама Halo2

Почему важно: Формальная верификация zkVM снижает риск подделки доказательств, от которых зависит безопасность ZK-мостов и L2.

Ещё по теме