Przejdź do głównej treści
Bezpieczeństwo i testowanie

Kontrol - formal verification tool based on Foundry and KEVM

Weryfikacja formalna

Zobacz na GitHubie (otwiera się w nowej karcie)Kontrol - formal verification tool based on Foundry and KEVM na X (otwiera się w nowej karcie)

Zobacz następne

Act

O Kontrol - formal verification tool based on Foundry and KEVM

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.

Tagi

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

Repozytoriaruntimeverification

Informacje

Typ
Weryfikacja formalna
Gwiazdki na GitHubie
127
Licencja
BSD-3-Clause
Przegląd wpisu
czerwiec 2026

Podobne narzędzia

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.

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.