The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar
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.
WALA-based Solidity static analysis. Currently it includes RoundAbout, a tool for inferring rounding direction across functions, expressions, and calls.
ERC-TRUST: a proposed Ethereum standard for typed regulatory actions and verifiable receipts on security tokens, with reference implementation and formal verification artifacts.
Formal verification effort for proving the ABDK Math 64.64 library properties using Echidna/hevm/Certora
Soroban lending protocol on Stellar.
Formal verification of Sarcophagus, the Autonomous and decentralized dead man's switch
A foundry project about formal verification testing using tools like Halmos and Certora.
Math Library Audit for Assembly & Formal Verification Training
ZeroMoon zETH - The Unbreakable Token
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
Claude Code / Agent Skill for writing CVL specs and formally verifying EVM smart contracts with the Certora Prover (CVL). Unofficial.
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.
To associate your repository with the certora topic, visit your repo's landing page and select "manage topics."