Security & testing

Kontrol - formal verification tool based on Foundry and KEVM

Formal verification

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

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

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.

Related resources

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 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 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 łą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ą.