Usalama na majaribio

K Semantics of the Ethereum Virtual Machine (EVM)

Uthibitishaji rasmi

Tazama kwenye GitHub

Tazama inayofuata

hax

Kuhusu 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.

Lebo

Usalama
Elimu
Uchanganuzi
Uthibitishaji rasmi
Utekelezaji wa kiishara
Zana za utatuzi
Uthibitishaji wa wakati wa utekelezaji
Vyper

Hifadhiruntimeverification

evm-semantics595 (inafunguka katika kichupo kipya)

Maelezo

Aina: Uthibitishaji rasmi
Nyota za GitHub: 595
Leseni: BSD-3-Clause
Orodha imekaguliwa: Juni 2026

Zana zinazofanana

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.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol inainua majaribio ya mali ya Foundry kuwa uthibitisho unaoungwa mkono na KEVM ili uweze kufuatilia dhamana rasmi kwa kazi ndogo ya vipimo vilivyoandikwa kwa mkono kuliko KEVM ghafi pekee.

Act

Act ni lugha ya ubainishaji ya kutangaza ya Ethereum na msururu wa zana kwa ajili ya kuelezea tabia zote za programu ya EVM ili vitatuzi vya SMT, wathibitishaji wa nadharia, au zana za uchanganuzi wa kiuchumi ziweze kufikiri kuhusu usahihi wa kiwango cha msimbo wa baiti na uoanifu wa motisha, ikijumuisha uthibitisho wa uboreshaji wa kiotomatiki dhidi ya utekelezaji halisi.