Passer au contenu principal
Sécurité et tests

Kontrol - formal verification tool based on Foundry and KEVM

Vérification formelle

Voir sur GitHub (s'ouvre dans un nouvel onglet)Kontrol - formal verification tool based on Foundry and KEVM sur X (s'ouvre dans un nouvel onglet)

Voir le suivant

Act

À propos de Kontrol - formal verification tool based on Foundry and KEVM

Kontrol élève les tests de propriétés de Foundry en preuves soutenues par KEVM afin que vous puissiez rechercher des garanties formelles avec moins de travail de spécification manuelle que le KEVM brut seul.

Tags

  • Foundry
  • Éducation
  • Gouvernance
  • Vérification formelle
  • Solidity
  • Vérification à l'exécution
  • Déploiement de contrat
  • Analyse statique

Dépôtsruntimeverification

Informations

Type
Vérification formelle
Étoiles GitHub
127
Licence
BSD-3-Clause
Fiche révisée
juin 2026

Outils similaires

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM est la sémantique exécutable du framework K de l'EVM : pointez-le vers le bytecode lorsque vous avez besoin d'une exécution vérifiée en termes de conformité, d'une exploration symbolique, d'un raisonnement sur le gaz ou de preuves qui suivent de près les règles d'Ethereum.

hax

hax

hax est un outil pour les traductions à haute assurance d'un grand sous-ensemble de Rust vers des langages formels tels que 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.