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

Act

Weryfikacja formalna

Zobacz na GitHubie (otwiera się w nowej karcie)

Zobacz następne

Verifereum

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

Tagi

  • Edukacja
  • Analityka
  • Weryfikacja formalna
  • Wykonywanie symboliczne

Repozytoriumethereum

Informacje

Typ
Weryfikacja formalna
Gwiazdki na GitHubie
284
Licencja
AGPL-3.0
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.