Agent skill

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.

a5c-aigithub.com/a5c-aiGitHub ↗
claude-codecodexcan modify filesMIT
Install
npx skills add a5c-ai/babysitter --skill certora-prover --agent claude-code

Same command for any agent — swap --agent for codex, cursor, copilot.

Facts
Files in the skill folder: 2
SKILL.md size: 8 KB
Bundled scripts: none
Allowed tools: ReadGrepWriteBashEditGlobWebFetch
Path: library/specializations/cryptography-blockchain/skills/certora-prover/SKILL.md
Open the folder on GitHub →
Where it comes from
Stars: 1,642
Language: JavaScript

Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.

From the SKILL.md

# 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 specs - **Invariant Rules**: Define and verify state invariants - **Parametric Rules**: Write comprehensive property tests - **Ghost Variables**: Track abstract state - **Counterexamples**: Analyze verification failures - **Loop Handling**: Configure loop invariants and unrolling - **Summarization**: Abstract complex functions ## Installation ```bash # 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 Setup ### Directory Structure ``` project/ ├── contracts/ │ └── Token.sol ├── certora/ │ ├── conf/ │ │ └── token.conf │ └── specs/ │ └── token.spec └── foundry.toml ``` ### Configuration File ```yaml # 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, "

What's inside
Steps it walks through
  1. Capabilities
  2. Installation
  3. Project Setup
  4. Directory Structure
  5. Configuration File
  6. CVL Specification Language
  7. Basic Rules
  8. Parametric Rules
  9. Ghost Variables
  10. Function Summaries
  11. Loop Handling
  12. Running Verification
  13. Basic Run
  14. Advanced Options
Ships with 1 file
  • README.md
Commands it runs
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
Run verification
certoraRun certora/conf/token.conf
More from babysitter
All skills →
generating-gcp-diagramsGenerates DrawIO XML diagrams for Google Cloud Platform architectures from text descriptions or…DevOps & Cloudgenerating-aws-diagramsGenerates DrawIO XML diagrams for Amazon Web Services architectures from text descriptions or…DevOps & Cloudcorrosion-materials-selectorMaterials selection skill for corrosion resistance based on process conditions and industry…AI & Agentsapi-diff-analyzerCompare API specifications to detect breaking changes. Compare OpenAPI spec versions, categorize…Databasesdistillation-designerDistillation column design skill for tray/packing selection, hydraulic analysis, and column…Design & Presentationcrystallizer-designerCrystallization process design skill for nucleation control, crystal size distribution, and…Design & Presentation
About this skill
What does the certora-prover skill do?

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.

How do I install it?

Run `npx skills add a5c-ai/babysitter --skill certora-prover --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.

Where does this skill come from?

From a5c-ai/babysitter, a repository with 1,642 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.

Is a popular skill a good skill?

Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.

Keep going
All skills →
The full catalog, by category and by tool.
Open Source Radar →
The repositories these skills come from, watched daily.
The people behind them →
Makers and builders across the ecosystem.