본문으로 건너뛰기
보안 및 테스트

Kontrol - formal verification tool based on Foundry and KEVM

정형 검증

View on GitHub (새 탭에서 열림)Kontrol - formal verification tool based on Foundry and KEVM on X (새 탭에서 열림)

See next

Act

About Kontrol - formal verification tool based on Foundry and KEVM

Kontrol은 Foundry 속성 테스트를 KEVM 기반 증명으로 끌어올려, 순수 KEVM만 사용할 때보다 수작업 사양 작성 작업을 줄이면서 정형 검증 보장을 추구할 수 있게 해줍니다.

태그

  • Foundry
  • 교육
  • 거버넌스
  • 정형 검증
  • Solidity
  • 런타임 검증
  • 컨트랙트 배포
  • 정적 분석

리포지토리runtimeverification

Info

유형
정형 검증
GitHub stars
126

관련 리소스

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM은 EVM의 K-프레임워크 실행 가능 의미론(executable semantics)입니다. 적합성 검사 실행, 기호 탐색, 가스 추론 또는 이더리움의 규칙을 면밀히 추적하는 증명이 필요할 때 바이트코드에 적용하세요.

hax

hax

hax는 Rust의 큰 하위 집합을 F* 또는 Rocq와 같은 공식 언어로 높은 보증(high assurance)을 가지고 번역하기 위한 도구입니다.

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.