Skip to main content
certora-prover Formal verification using Certora Prover with CVL specification language. Supports invariant rules, parametric verification, ghost variables, and counterexample analysis for mathematical proof of contract correctness.
Jump to install Skills Marketplace Discover and explore AI skills built by the community.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
Show prompt details A direct command skips the review prompt. Inspect the source before running it.
npx skills add https://github.com/a5c-ai/babysitter --skill certora-proverThe command stays on one line. Scroll horizontally to inspect it before copying.
Prefer a local copy? Download the files currently available to SkillsMP.
Download Zip Downloading... More from this repository Reference for querying the Atlas knowledge graph through its MCP tools โ the SECONDARY enrichment/comparison layer that adds best-practice context to systems you have ALREADY scanned from your real sources (`az`, repos, dirs). Use when you need to look up nodes, edges, kinds, clusters, stats, or wiki pages in Atlas to compare against your real inventory. (atlas graph, query atlas, atlas mcp, search the graph, graph neighbors, atlas record, atlas kinds, enrichment layer)
Atlas turns your STATED NEED into a real systems atlas by SCANNING your actual sources (Azure via `az`, git repos, local dirs) and process/data mining them, THEN enriching against the Atlas knowledge graph. Use this skill when asked to inventory/map your real systems, scan your cloud + repos + directories, mine the real processes or data they contain, or collect their real constraints/gotchas. (atlas, scan my systems, inventory our azure account, map my repos, real systems atlas, process mining, data mining, collect nuances, system discovery)
assimilate-popular-workflows This skill should be used when the user asks to "find skills in the wild", "assimilate popular workflows", "discover SKILL.md files in repos", "research external skills", "find workflow patterns", "survey the skill landscape", "what skills exist out there", or wants to investigate public repositories for extractable processes, babysitter plugins, and reusable procedural insights. Searches GitHub for SKILL.md files, classifies repos by archetype, and maintains structured research under docs/reference-repos/.
Related occupations SOC
Based on SOC occupation classification
name certora-prover description Formal verification using Certora Prover with CVL specification language. Supports invariant rules, parametric verification, ghost variables, and counterexample analysis for mathematical proof of contract correctness. allowed-tools Read, Grep, Write, Bash, Edit, Glob, WebFetch graph {"domains":["domain:security"],"specializations":["specialization:cryptography-blockchain"],"skillAreas":["skill-area:smart-contract-security","skill-area:smart-contract-development-testing","skill-area:application-security-testing"],"roles":["role:security-engineer"]}
Certora Formal Verification Skill
Formal verification of smart contracts using Certora Prover, providing mathematical proofs of contract correctness.
Capabilities
CVL Specifications : Write Certora Verification Language specsInvariant Rules : Define and verify state invariantsParametric Rules : Write comprehensive property testsGhost Variables : Track abstract stateCounterexamples : Analyze verification failuresLoop Handling : Configure loop invariants and unrollingSummarization : Abstract complex functions
Installation
sudo apt install openjdk-17-jdk
export
Project Setup
Directory Structure project/
โโโ contracts/
โ โโโ Token.sol
โโโ certora/
โ โโโ conf/
โ โ โโโ token.conf
โ โโโ specs/
โ โโโ token.spec
โโโ foundry.toml
Configuration File
{
"files": ["contracts/Token.sol" ],
"verify": "Token:certora/specs/token.spec" ,
"solc": "solc-0.8.20" ,
"msg": "Token verification" ,
"rule_sanity": "basic" ,
"optimistic_loop": true ,
"loop_iter": 3
}
CVL Specification Language
Basic Rules // certora/specs/token.spec
methods {
function balanceOf(address) external returns (uint256) envfree;
function totalSupply() external returns (uint256) envfree;
function transfer(address, uint256) external returns (bool);
}
// Invariant: balance never exceeds total supply
invariant balanceUnderSupply(address user)
balanceOf(user) <= totalSupply()
// Rule: transfer preserves total supply
rule transferPreservesTotalSupply(address to, uint256 amount) {
env e;
uint256 supplyBefore = totalSupply();
transfer(e, to, amount);
uint256 supplyAfter = totalSupply();
assert supplyBefore == supplyAfter,
"Total supply changed after transfer";
}
Parametric Rules // Parametric rule: any function preserves an invariant
rule anyFunctionPreservesInvariant(method f) {
env e;
calldataarg args;
uint256 supplyBefore = totalSupply();
f(e, args);
uint256 supplyAfter = totalSupply();
assert supplyBefore == supplyAfter,
"Total supply changed";
}
Ghost Variables // Ghost variable to track sum of all balances
ghost mathint sumBalances {
init_state axiom sumBalances == 0;
}
// Hook to update ghost on balance changes
hook Sstore balances[KEY address user] uint256 newBalance
(uint256 oldBalance) STORAGE {
sumBalances = sumBalances + newBalance - oldBalance;
}
// Invariant using ghost
invariant totalSupplyIsSumOfBalances()
to_mathint(totalSupply()) == sumBalances
Function Summaries // Summary for external calls
methods {
function _.transfer(address, uint256) external => DISPATCHER(true);
function _.balanceOf(address) external returns (uint256) => DISPATCHER(true);
}
// Havoc summary (non-deterministic)
methods {
function externalCall() external => HAVOC_ECF;
}
// Constant summary
methods {
function getConstant() external returns (uint256) => ALWAYS(100);
}
Loop Handling // Loop invariant
rule loopInvariant() {
env e;
// Configure loop unrolling
require e.msg.sender != 0;
// Loop iterations are bounded by config
processArray(e);
assert true; // Verify loop terminates
}
Running Verification
Basic Run
certoraRun certora/conf/token.conf
certoraRun certora/conf/token.conf --rule transferPreservesTotalSupply
certoraRun certora/conf/token.conf --msg "PR #123 verification"
Advanced Options
certoraRun certora/conf/token.conf --rule_sanity basic
certoraRun certora/conf/token.conf --optimistic_loop --loop_iter 5
certoraRun contracts/Token.sol contracts/Staking.sol \
--verify Token:specs/token.spec
certoraRun certora/conf/token.conf --debug
Interpreting Results
Verification Output Rule: transferPreservesTotalSupply
Status: VERIFIED โ
Time: 45s
Rule: balanceUnderSupply
Status: VIOLATED โ
Counterexample:
- user: 0x1234...
- Initial balance: 100
- Final balance: 200
- Total supply: 150
Counterexample Analysis
Check Call Trace : Understand the sequence of callsExamine State Changes : Track storage modificationsIdentify Assumptions : Check if assumptions are too weakVerify Model : Ensure CVL spec matches intent
Common Patterns
ERC-20 Verification methods {
function balanceOf(address) external returns (uint256) envfree;
function totalSupply() external returns (uint256) envfree;
function allowance(address, address) external returns (uint256) envfree;
}
// Transfer integrity
rule transferIntegrity(address to, uint256 amount) {
env e;
address from = e.msg.sender;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
require from != to;
transfer(e, to, amount);
uint256 fromBalanceAfter = balanceOf(from);
uint256 toBalanceAfter = balanceOf(to);
assert fromBalanceAfter == fromBalanceBefore - amount;
assert toBalanceAfter == toBalanceBefore + amount;
}
// Allowance monotonicity
rule approveIntegrity(address spender, uint256 amount) {
env e;
approve(e, spender, amount);
assert allowance(e.msg.sender, spender) == amount;
}
Access Control Verification methods {
function owner() external returns (address) envfree;
function setOwner(address) external;
}
// Only owner can change owner
rule onlyOwnerCanChangeOwner(address newOwner) {
env e;
address ownerBefore = owner();
setOwner(e, newOwner);
assert e.msg.sender == ownerBefore,
"Non-owner changed owner";
}
CI/CD Integration
GitHub Actions name: Certora Verification
on: [push , pull_request ]
jobs:
certora:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Install Certora
run: pip install certora-cli
- name: Run Verification
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}
run: certoraRun certora/conf/token.conf
Process Integration Process Purpose formal-verification.jsPrimary verification smart-contract-security-audit.jsDeep security analysis lending-protocol.jsProtocol correctness amm-pool-development.jsDeFi invariants governance-system.jsGovernance properties
Best Practices
Start with simple invariants
Use parametric rules for comprehensive coverage
Document all assumptions
Analyze counterexamples carefully
Use ghost variables for complex state tracking
Set appropriate loop bounds
Run nightly verification in CI
See Also
skills/slither-analysis/SKILL.md - Static analysisskills/echidna-fuzzer/SKILL.md - Property fuzzingagents/formal-methods/AGENT.md - Verification expertCertora Documentation 