zksecurity запустила челлендж на как можно более дешёвую формальную верификацию zk‑схем на lean4, но из‑за лазейки в методике проверки QED audit захватил таблицу лидеров

zksecurity запустили челлендж на максимально дешёвую формальную верификацию zk‑схем в lean4... Оказалось, в методике проверки есть лазейка, так что QED audit просто оккупировали лидерборд.

В челлендже при проверке корректности и полноты используют импликацию вида p -> q; если p ложно, импликация всегда истинна, так что, похоже, они просто поставили везде ложное p и прошли проверку (не уверен, что так и было).

Объяснение: https://x.com/QED_Audit/status/2075400032937775326?s=20