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.
Verifies smart contract correctness using formal methods with Certora Prover and CVL specifications.
npx claudepluginhub a5c-ai/babysitterThis skill is limited to using the following tools:
README.mdFormal verification of smart contracts using Certora Prover, providing mathematical proofs of contract correctness.
# Install Java (required)
sudo apt install openjdk-17-jdk
# Install Certora CLI
pip install certora-cli
# Set API key
export CERTORAKEY=<your-api-key>
# Verify installation
certoraRun --version
project/
├── contracts/
│ └── Token.sol
├── certora/
│ ├── conf/
│ │ └── token.conf
│ └── specs/
│ └── token.spec
└── foundry.toml
# certora/conf/token.conf
{
"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
}
// 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 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 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
// 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 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
}
# Run verification
certoraRun certora/conf/token.conf
# Run specific rule
certoraRun certora/conf/token.conf --rule transferPreservesTotalSupply
# Run with message
certoraRun certora/conf/token.conf --msg "PR #123 verification"
# Sanity checks
certoraRun certora/conf/token.conf --rule_sanity basic
# Optimistic loop handling
certoraRun certora/conf/token.conf --optimistic_loop --loop_iter 5
# Multi-contract verification
certoraRun contracts/Token.sol contracts/Staking.sol \
--verify Token:specs/token.spec
# Debug mode
certoraRun certora/conf/token.conf --debug
Rule: transferPreservesTotalSupply
Status: VERIFIED ✓
Time: 45s
Rule: balanceUnderSupply
Status: VIOLATED ✗
Counterexample:
- user: 0x1234...
- Initial balance: 100
- Final balance: 200
- Total supply: 150
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;
}
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";
}
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 | Purpose |
|---|---|
formal-verification.js | Primary verification |
smart-contract-security-audit.js | Deep security analysis |
lending-protocol.js | Protocol correctness |
amm-pool-development.js | DeFi invariants |
governance-system.js | Governance properties |
skills/slither-analysis/SKILL.md - Static analysisskills/echidna-fuzzer/SKILL.md - Property fuzzingagents/formal-methods/AGENT.md - Verification expertActivates when the user asks about AI prompts, needs prompt templates, wants to search for prompts, or mentions prompts.chat. Use for discovering, retrieving, and improving prompts.
Search, retrieve, and install Agent Skills from the prompts.chat registry using MCP tools. Use when the user asks to find skills, browse skill catalogs, install a skill for Claude, or extend Claude's capabilities with reusable AI agent components.
This skill should be used when the user wants to "create a skill", "add a skill to plugin", "write a new skill", "improve skill description", "organize skill content", or needs guidance on skill structure, progressive disclosure, or skill development best practices for Claude Code plugins.