Verifereum

إن ⁦KEVM⁩ هي الدلالات القابلة للتنفيذ لإطار عمل ⁦K⁩ لـ ⁦EVM⁩: وجهها إلى رمز البايت عندما تحتاج إلى تنفيذ تم التحقق من توافقه، أو استكشاف رمزي، أو استنتاج الغاز، أو إثباتات تتتبع قواعد إيثيريوم عن كثب.

إن ⁦hax⁩ هي أداة لترجمات عالية الضمان لمجموعة فرعية كبيرة من ⁦Rust⁩ إلى لغات رسمية مثل ⁦F*⁩ أو ⁦Rocq⁩.

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.