Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

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

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

Related resources

Kontrol - formal verification tool based on Foundry and KEVM

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

hax

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

Act

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

Verifereum

Verifereum은 이더리움 스마트 컨트랙트를 HOL4 기반 정리 증명에 연결하여 자동화된 SMT 접근 방식이 충분하지 않을 때 매우 강력한 정확성 주장을 목표로 할 수 있도록 합니다.