certora 开源项目推荐（18 个）

Certora /CertoraProver

Certora Prover 是运行在基于 EVM 链、Solana 和 Stellar 的智能合约的自动化形式验证安全工具

Certora /SecurityReports

Certora's Formal Verification and Audit Portfolio – a comprehensive collection of smart contract security verification reports and audits for leading Web3 protocols on EVM-based chains, Solana, and Stellar.

Certora /wala-solidity

WALA-based Solidity static analysis. Currently it includes RoundAbout, a tool for inferring rounding direction across functions, expressions, and calls.

Oraclizer /erc-trust

ERC-TRUST: a proposed Ethereum standard for typed regulatory actions and verifiable receipts on security tokens, with reference implementation and formal verification artifacts.

gustavo-grieco /abdk-math-64.64-verification

Formal verification effort for proving the ABDK Math 64.64 library properties using Echidna/hevm/Certora

XOXNO /rs-lending-xlm

Soroban lending protocol on Stellar.

EGmux /Sarcophagus_certora_formal-verification

Formal verification of Sarcophagus, the Autonomous and decentralized dead man's switch

scab24 /Formal_Verification

该项目在 GitHub 上没有填写描述

TSxo /evm-security-tools

Dockerfile for building an image pre-installed and pre-configured with essential EVM security tools

kukushking /fvharness

Formal verification of smart contracts: Certora CVL spec generation harness with mutation-coverage scoring. June 2026.

GushALKDev /formal-verification-math-master-audit

Math Library Audit for Assembly & Formal Verification Training

Meharab /Security-Audit-Portfolio

该项目在 GitHub 上没有填写描述

ZeroMoonETH /zETH

ZeroMoon zETH - The Unbreakable Token

dt6120 /math-master-fv

A foundry project about formal verification testing using tools like Halmos and Certora.

jose-compu /smart-contract-verification

Survey of smart-contract verification methods (Lean, Certora CVL, Alloy, Halmos, and others).

Jackesgamero /smart-contract-security-lab

A benchmark of intentionally vulnerable smart contracts aligned with the SWC registry, built to evaluate formal verification tools including SolCMC, Certora, eThor, HoRStify, and Securify2

zakrad /certora-prover-skill

Claude Code / Agent Skill for writing CVL specs and formally verifying EVM smart contracts with the Certora Prover (CVL). Unofficial.

harshit391 /Secure-Smart-Contract-Permission-And-Key-Management-Pattern-Formal-Verification-and-Java-Tooling

Formally verified Solidity design patterns for smart-contract permission & key management: k-of-n multisig wallet, timelock controller, and RBAC manager — verified via Slither, Mythril, and Certora (10 safety invariants). Includes a Java/web3j CI toolkit. 35/35 tests passing, 0 vulnerabilities. Research paper (IEEE format) included.