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

hax

Verificação formal

Visitar site (abre em uma nova aba)hax em GitHub (abre em uma nova aba)

Ver próximo

Certora Prover

Sobre hax

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

Tags

  • Verificação formal

Repositóriocryspen

Informações

Tipo
Verificação formal
Estrelas no GitHub
502
Licença
Apache-2.0
Listagem revisada
julho 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.

Kontrol - formal verification tool based on Foundry and KEVM

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

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.