Pular para o conteúdo principal
Segurança e testes

Verifereum

Verificação formal

Visit website (abre em uma nova aba)Verifereum on X (abre em uma nova aba)Verifereum on GitHub (abre em uma nova aba)

See next

Certora AutoProver

About Verifereum

O Verifereum conecta contratos inteligentes do Ethereum à prova de teoremas apoiada por HOL4 para que você possa buscar alegações de correção muito fortes quando as abordagens SMT automatizadas não forem suficientes.

Tags

  • Segurança
  • Educação
  • Verificação formal

Repositórioverifereum

Info

Tipo
Verificação formal
GitHub stars
54

Recursos relacionados

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

A KEVM é a semântica executável do K-framework da EVM: aponte-a para o bytecode quando precisar de execução com verificação de conformidade, exploração simbólica, raciocínio de gás ou provas que acompanhem de perto as regras do Ethereum.

hax

hax

O hax é uma ferramenta para traduções de alta garantia de um grande subconjunto de Rust para linguagens formais como F* ou 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.