Bezpieczeństwo i testowanie

Certora Prover

Weryfikacja formalna

Zobacz na GitHubie

Zobacz następne

Kontrol - formal verification tool based on Foundry and KEVM

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

Tagi

Weryfikacja formalna
Weryfikacja
Bezpieczeństwo

RepozytoriumCertora

CertoraProver339 (otwiera się w nowej karcie)

Informacje

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

Podobne narzędzia

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

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.