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

Kontrol - formal verification tool based on Foundry and KEVM

Verificação formal

Ver no GitHub (abre em uma nova aba)Kontrol - formal verification tool based on Foundry and KEVM em X (abre em uma nova aba)

Ver próximo

Act

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

Tags

  • Foundry
  • Educação
  • Governança
  • Verificação formal
  • Solidity
  • Verificação em tempo de execução
  • Implantação de contrato
  • Análise estática

Repositóriosruntimeverification

Informações

Tipo
Verificação formal
Estrelas no GitHub
127
Licença
BSD-3-Clause
Listagem revisada
junho de 2026

Ferramentas semelhantes

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.