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

K Semantics of the Ethereum Virtual Machine (EVM)

정형 검증

View on GitHub (새 탭에서 열림)K Semantics of the Ethereum Virtual Machine (EVM) on X (새 탭에서 열림)

See next

hax

About K Semantics of the Ethereum Virtual Machine (EVM)

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

태그

  • 보안
  • 교육
  • 분석
  • 정형 검증
  • 심볼릭 실행
  • 디버깅 도구
  • 런타임 검증
  • Vyper

리포지토리runtimeverification

Info

유형
정형 검증
GitHub stars
595
License
BSD-3-Clause
Listing reviewed
2026년 6월

관련 리소스

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.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

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

Act

Act

Act는 EVM 프로그램의 모든 동작을 설명하기 위한 이더리움의 선언적 사양 언어 및 툴체인으로, SMT 솔버, 정리 증명기 또는 경제 분석 도구가 구체적인 구현에 대한 자동 정제 증명을 포함하여 바이트코드 수준의 정확성과 인센티브 호환성을 추론할 수 있도록 합니다.