보안 및 테스트

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.

관련 리소스

K Semantics of the Ethereum Virtual Machine (EVM)

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

hax

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

Kontrol - formal verification tool based on Foundry and KEVM

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

Act

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

Certora AutoProver

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

Verifereum

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