Segurança e testes

Certora Prover

Verificação formal

Verificação formal · Verificação · Segurança

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.

Recursos relacionados

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

O hax é uma ferramenta para traduções de alta garantia de um grande subconjunto de Rust para linguagens formais como F* ou Rocq.

Kontrol - formal verification tool based on Foundry and KEVM

O Kontrol eleva os testes de propriedade do Foundry a provas apoiadas pela KEVM para que você possa buscar garantias formais com menos trabalho de especificação manual do que apenas com a KEVM bruta.

Act

O Act é a linguagem de especificação declarativa e o conjunto de ferramentas do Ethereum para descrever todos os comportamentos de um programa EVM, para que solucionadores SMT, provadores de teoremas ou ferramentas de análise econômica possam raciocinar sobre a correção no nível do bytecode e a compatibilidade de incentivos, incluindo provas de refinamento automático contra implementações concretas.

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.

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.