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

K Semantics of the Ethereum Virtual Machine (EVM)

Weryfikacja formalna

Zobacz na GitHubie (otwiera się w nowej karcie)K Semantics of the Ethereum Virtual Machine (EVM) na X (otwiera się w nowej karcie)

Zobacz następne

hax

O 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.

Tagi

  • Bezpieczeństwo
  • Edukacja
  • Analityka
  • Weryfikacja formalna
  • Wykonywanie symboliczne
  • Narzędzia do debugowania
  • Weryfikacja w czasie wykonywania
  • Vyper

Repozytoriumruntimeverification

Informacje

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

Podobne narzędzia

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.

Kontrol - formal verification tool based on Foundry and KEVM

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.

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.