Přejít na hlavní obsah
Kontrol - formal verification tool based on Foundry and KEVM
Security & testing

Kontrol - formal verification tool based on Foundry and KEVM

Formal verification

Foundry · Vzdělávání · Správa · Formální verifikace · Solidity · Verifikace za běhu · Nasazení kontraktu · Statická analýza

Sociální sítě (opens in a new tab)runtimeverification/kontrol(118 ☆) (opens in a new tab)runtimeverification/optimism-ci(4 ☆) (opens in a new tab)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆) (opens in a new tab)runtimeverification/yearn-v3-term-vault(0 ☆) (opens in a new tab)runtimeverification/Depeg-swap(0 ☆) (opens in a new tab)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆) (opens in a new tab)

Kontrol povyšuje testy vlastností ve Foundry na důkazy podložené KEVM, takže můžete usilovat o formální záruky s menším množstvím ručně psaných specifikací než u samotného čistého KEVM.

Related resources

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM je spustitelná sémantika EVM v K-frameworku: namiřte ji na bajtkód, když potřebujete provádění s kontrolou shody, symbolické zkoumání, uvažování o gasu nebo důkazy, které přesně sledují pravidla Etherea.

hax

hax je nástroj pro vysoce spolehlivé překlady velké podmnožiny jazyka Rust do formálních jazyků, jako jsou F* nebo Rocq.

Act

Act

Act je deklarativní specifikační jazyk a sada nástrojů Etherea pro popis veškerého chování EVM programu, aby SMT řešiče, dokazovače teorémů nebo nástroje pro ekonomickou analýzu mohly uvažovat o správnosti na úrovni bajtkódu a kompatibilitě pobídek, včetně automatických důkazů zjemnění vůči konkrétním implementacím.

Verifereum

Verifereum

Verifereum propojuje chytré kontrakty Etherea s dokazováním teorémů podporovaným HOL4, takže můžete cílit na velmi silná tvrzení o správnosti, když automatizované přístupy SMT nestačí.