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

Certora Prover

정형 검증

GitHub에서 보기 (새 탭에서 열림)

다음 보기

Kontrol - formal verification tool based on Foundry and KEVM

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.

태그

  • 정형 검증
  • 검증
  • 보안

리포지토리Certora

정보

유형
정형 검증
GitHub 스타
339
라이선스
GPL-3.0
리스팅 검토일
2026년 9월

유사한 도구

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)을 가지고 번역하기 위한 도구입니다.

Act

Act

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