Vai al contenuto principale
Sicurezza e testing

Certora AutoProver

Verifica formale

Visualizza su GitHub (si apre in una nuova scheda)

Vedi il prossimo

K Semantics of the Ethereum Virtual Machine (EVM)

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

Tag

  • Verifica formale
  • Verifica

RepositoryCertora

Info

Tipo
Verifica formale
Stelle su GitHub
17
Licenza
GPL-3.0
Scheda revisionata
settembre 2026

Strumenti simili

hax

hax

hax è uno strumento per traduzioni ad alta garanzia di un ampio sottoinsieme di Rust in linguaggi formali come F* o 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 eleva i test delle proprietà di Foundry in prove supportate da KEVM, in modo da poter perseguire garanzie formali con meno lavoro di specifica scritto a mano rispetto al solo KEVM grezzo.