Vai al contenuto principale
Sicurezza e testing

Kontrol - formal verification tool based on Foundry and KEVM

Verifica formale

Visualizza su GitHub (si apre in una nuova scheda)Kontrol - formal verification tool based on Foundry and KEVM su X (si apre in una nuova scheda)

Vedi il prossimo

Act

Informazioni su Kontrol - formal verification tool based on Foundry and KEVM

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.

Tag

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

Repositoryruntimeverification

Info

Tipo
Verifica formale
Stelle su GitHub
127
Licenza
BSD-3-Clause
Scheda revisionata
giugno 2026

Strumenti simili

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.

Certora Prover

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.