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

Certora AutoProver

Weryfikacja formalna

Zobacz na GitHubie (otwiera się w nowej karcie)

Zobacz następne

K Semantics of the Ethereum Virtual Machine (EVM)

O Certora AutoProver

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

Tagi

  • Weryfikacja formalna
  • Weryfikacja

RepozytoriumCertora

Informacje

Typ
Weryfikacja formalna
Gwiazdki na GitHubie
17
Licencja
GPL-3.0
Przegląd wpisu
wrzesień 2026

Podobne narzędzia

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.

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.