Skip to main content
Security & testing

Verifereum

Formal verification

Visit website (opens in a new tab)Verifereum on X (opens in a new tab)Verifereum on GitHub (opens in a new tab)

See next

Certora AutoProver

About Verifereum

Verifereum connects Ethereum smart contracts to HOL4-backed theorem proving so you can aim at very strong correctness claims when automated SMT approaches are not enough.

Tags

  • Security
  • Education
  • Formal verification

Repositoryverifereum

Info

Type
Formal verification
GitHub stars
54

Similar tools

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM is the K-framework executable semantics of the EVM: point it at bytecode when you need conformance-checked execution, symbolic exploration, gas reasoning, or proofs that track Ethereum's rules closely.

hax

hax

hax is a tool for high assurance translations of a large subset of Rust into formal languages such as F* or 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.