Przejdź do głównej treści
Kontrol - formal verification tool based on Foundry and KEVM
Bezpieczeństwo i testowanie

Kontrol - formal verification tool based on Foundry and KEVM

Weryfikacja formalna

Foundry · Edukacja · Zarządzanie · Weryfikacja formalna · Solidity · Weryfikacja w czasie wykonywania · Wdrożenie kontraktu · Analiza statyczna

Społeczności (otwiera się w nowej karcie)runtimeverification/kontrol(118 ☆) (otwiera się w nowej karcie)runtimeverification/optimism-ci(4 ☆) (otwiera się w nowej karcie)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆) (otwiera się w nowej karcie)runtimeverification/yearn-v3-term-vault(0 ☆) (otwiera się w nowej karcie)runtimeverification/Depeg-swap(0 ☆) (otwiera się w nowej karcie)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆) (otwiera się w nowej karcie)

Kontrol podnosi testy właściwości Foundry do dowodów opartych na KEVM, dzięki czemu możesz dążyć do formalnych gwarancji przy mniejszej ilości ręcznie pisanej specyfikacji niż w przypadku samego KEVM.

Powiązane zasoby

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM to wykonywalna semantyka EVM w K-framework: wskaż jej kod bajtowy, gdy potrzebujesz wykonania ze sprawdzeniem zgodności, eksploracji symbolicznej, wnioskowania o gazie lub dowodów, które ściśle śledzą zasady Ethereum.

hax

hax

hax to narzędzie do tłumaczeń o wysokiej pewności (high assurance) dużego podzbioru języka Rust na języki formalne, takie jak F* lub Rocq.

Act

Act

Act to deklaratywny język specyfikacji i zestaw narzędzi Ethereum do opisywania wszystkich zachowań programu EVM, dzięki czemu solvery SMT, systemy dowodzenia twierdzeń lub narzędzia analizy ekonomicznej mogą wnioskować o poprawności na poziomie kodu bajtowego i kompatybilności zachęt, w tym o automatycznych dowodach udoskonalenia w stosunku do konkretnych implementacji.

Verifereum

Verifereum

Verifereum łączy inteligentne kontrakty Ethereum z dowodzeniem twierdzeń opartym na HOL4, dzięki czemu możesz dążyć do bardzo silnych gwarancji poprawności, gdy zautomatyzowane podejścia SMT nie wystarczają.