Formal/symbolic properties on Solidity with Halmos, solc SMTChecker, Certora CVL, and Kontrol. Use when fuzzing is not enough for a conservation law. Slow path, like Mythril.
Scanned 9/2/2026
Install to Claude Code
Skills Directorynpx -y skills add nuroctane/nur-cli --skill formal-verification-halmos-certora-kontrol --agent claude-codeInstalls into .claude/skills of the current project.
Are you the author of Formal Verification Halmos Certora Kontrol?
Add the live security badge to your README — it updates automatically with every re-scan.
[](https://www.skillsdirectory.com/skills/nuroctane-formal-verification-halmos-certora-kontrol)More formats (shields.io, HTML) on the badges page.
---
name: formal-verification-halmos-certora-kontrol
description: "Formal/symbolic properties on Solidity with Halmos, solc SMTChecker, Certora CVL, and Kontrol. Use when fuzzing is not enough for a conservation law. Slow path, like Mythril."
---
# Formal verification (Halmos, Certora, Kontrol, SMTChecker)
In-scope. Start with Foundry invariants. Promote the law to a prover when the user asks or when the property is small and huge-value.
## Halmos (a16z)
Foundry tests that use `vm.assume` / symbolic `uint256`. Run `halmos --function check_`. Good for arithmetic and access control. Bounded loops.
## SMTChecker
`solc --model-checker-engine chc` or `pragma` annotations. Fast on small contracts; explodes on complex DeFi.
## Certora CVL
Specs in `.spec` files. Use when the project already has Certora CI. Do not invent a full CVL suite unprompted.
## Kontrol (Runtime Verification)
Foundry + K. Use when the repo already has `kontrol` proofs.
## Mythril
Still in the Foundry skill. Timeout 300s on the highest-value contract only.
Output: a property that **proved**, a counterexample (turn into a Foundry test), or "bound exhausted" (not a pass).
Is this your skill, or is something wrong with this listing? Request removal or report an issue. Author removals are honored within 72 hours.
No comments yet. Be the first to comment!
Ultra-compressed communication mode. Cuts token usage ~75% by speaking like caveman while keeping full technical accuracy. Supports intensity levels: lite, full (default), ultra, wenyan-lite, wenyan-full, wenyan-ultra. Use when user says "caveman mode", "talk like caveman", "use caveman", "less tokens", "be brief", or invokes /caveman. Also auto-triggers when token efficiency is requested.
Adversarial multi-agent planning skill. Self-orchestrates 5 hostile category members (unspecified-low, unspecified-high, deep, ultrabrain, artistry) via team-mode for ruthless cross-critique debate, distills only the defensible insights, then MANDATORILY hands the distilled insight bundle to the `plan` agent for executable plan formalization. Use when planning needs maximum rigor and surfacing of weak assumptions, blind spots, and over-engineering. Triggers: 'hyperplan', 'hpp', '/hyperplan', ...
**Complete production-ready guide for Google Gemini embeddings API** This skill provides comprehensive coverage of the `gemini-embedding-001` model for generating text embeddings, including SDK usage, REST API patterns, batch processing, RAG integration with Cloudflare Vectorize, and advanced use cases like semantic search and document clustering. ---
Interview, source-challenge, verify, save, and ADR-gate fuzzy coding requests into Codex-ready implementation specs. Use when a feature, bugfix, refactor, migration, repo-wide change, or architecture task needs user-verified requirements, source-backed decisions, durable architecture decisions, acceptance criteria, validation commands, rollout notes, saved spec/ADR files, and a Codex execution prompt. Do not use when already fully specified or when the user wants direct implementation now.
Use when a repo needs CodeGraph plus ast-grep for Codex MCP setup, exploration, impact analysis, structural search, or safe refactor planning.
