Usalama na majaribio

Verifereum

Uthibitishaji rasmi

Tembelea tovuti

Tazama inayofuata

Certora AutoProver

Kuhusu Verifereum

Verifereum inaunganisha mikataba mahiri ya Ethereum na uthibitishaji wa nadharia unaoungwa mkono na HOL4 ili uweze kulenga madai yenye nguvu sana ya usahihi wakati mbinu za kiotomatiki za SMT hazitoshi.

Lebo

Usalama
Elimu
Uthibitishaji rasmi

Hifadhiverifereum

verifereum54 (inafunguka katika kichupo kipya)

Maelezo

Aina: Uthibitishaji rasmi
Nyota za GitHub: 54
Leseni: GPL-3.0
Orodha imekaguliwa: Juni 2026

Zana zinazofanana

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM ni semantiki inayoweza kutekelezwa ya K-framework ya EVM: ielekeze kwenye msimbo wa baiti unapohitaji utekelezaji uliokaguliwa kwa kufuata, uchunguzi wa kiishara, hoja za gesi, au uthibitisho unaofuatilia sheria za Ethereum kwa karibu.

hax

hax ni zana ya tafsiri za uhakika wa juu za kitengo kikubwa cha Rust katika lugha rasmi kama vile F* au Rocq.

Certora Prover

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.