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

Verifereum

Weryfikacja formalna

Odwiedź stronę (otwiera się w nowej karcie)Verifereum na X (otwiera się w nowej karcie)Verifereum na GitHub (otwiera się w nowej karcie)

Zobacz następne

Certora AutoProver

O Verifereum

Verifereum łączy inteligentne kontrakty Ethereum z dowodzeniem twierdzeń opartym na HOL4, dzięki czemu możesz dążyć do bardzo silnych gwarancji poprawności, gdy zautomatyzowane podejścia SMT nie wystarczają.

Tagi

  • Bezpieczeństwo
  • Edukacja
  • Weryfikacja formalna

Repozytoriumverifereum

Informacje

Typ
Weryfikacja formalna
Gwiazdki na GitHubie
54
Licencja
GPL-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.