Vai al contenuto principale
Kontrol - formal verification tool based on Foundry and KEVM
Sicurezza e testing

Kontrol - formal verification tool based on Foundry and KEVM

Verifica formale

Foundry · Formazione · Governance · Verifica formale · Solidity · Verifica a runtime · Distribuzione del contratto · Analisi statica

Social (si apre in una nuova scheda)runtimeverification/kontrol(118 ☆) (si apre in una nuova scheda)runtimeverification/optimism-ci(4 ☆) (si apre in una nuova scheda)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆) (si apre in una nuova scheda)runtimeverification/yearn-v3-term-vault(0 ☆) (si apre in una nuova scheda)runtimeverification/Depeg-swap(0 ☆) (si apre in una nuova scheda)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆) (si apre in una nuova scheda)

Kontrol eleva i test delle proprietà di Foundry in prove supportate da KEVM, in modo da poter perseguire garanzie formali con meno lavoro di specifica scritto a mano rispetto al solo KEVM grezzo.

Risorse correlate

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM è la semantica eseguibile del K-framework dell'EVM: puntalo al bytecode quando hai bisogno di un'esecuzione con controllo di conformità, esplorazione simbolica, ragionamento sul gas o prove che seguono da vicino le regole di Ethereum.

hax

hax

hax è uno strumento per traduzioni ad alta garanzia di un ampio sottoinsieme di Rust in linguaggi formali come F* o Rocq.

Act

Act

Act è il linguaggio di specifica dichiarativa e la toolchain di Ethereum per descrivere tutti i comportamenti di un programma EVM, in modo che i risolutori SMT, i dimostratori di teoremi o gli strumenti di analisi economica possano ragionare sulla correttezza a livello di bytecode e sulla compatibilità degli incentivi, incluse le prove di raffinamento automatico rispetto a implementazioni concrete.

Verifereum

Verifereum

Verifereum connette gli smart contract di Ethereum alla dimostrazione di teoremi supportata da HOL4, in modo da poter puntare a dichiarazioni di correttezza molto forti quando gli approcci SMT automatizzati non sono sufficienti.