Individual skill
formal-verification
Use when applying formal verification to Solidity contracts using Certora CVL or Halmos symbolic testing. Covers specification writing, rule types, ghost variables, hooks, and common verification patterns.
skills/formal-verification/SKILL.md
Source commit a53141f10a1bbf9c634e44af6bc5a29dd1660697
What was checked
- Matches the observed repository HEAD
- Yes
- Scanner rules are current
- No
- Repository scan complete
- No
- Skill scan complete
- No
- Observed behavior
- Not checked yet
- Last checked
- Nov 7, 2026
These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.
Install this skill
Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.
An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.
Repository context
- Repository stars (not skill ratings)
- 132
- Repository last updated
- Oct 23, 2026
- License
- MIT
Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.
Files and excerpt
File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.
Read excerpt
# Formal Verification for Solidity
## Tools
| Tool | Approach | Strengths |
|------|----------|-----------|
| Certora Prover | CVL specs + SMT solving | Industry standard, deep analysis |
| Halmos | Symbolic Foundry tests | Familiar Foundry interface, open source |
| KEVM | K Framework semantics | EVM bytecode level verification |
## Certora CVL Specification Template
```cvl
// spec/Vault.spec