Halmos Verification — Testing & QA agent for Claude Code
Converts structured invariant specifications into compilable Halmos symbolic test suites (.t.sol) that run inside Foundry.
How to install Halmos Verification
Installs to ~/.claude/agents/calc1f4r-horus-halmos-verification.md
mkdir -p ~/.claude/agents && curl -fsSL https://raw.githubusercontent.com/calc1f4r/Horus/HEAD/.claude/agents/halmos-verification.md -o ~/.claude/agents/calc1f4r-horus-halmos-verification.md Restart Claude Code, or start a new session, for it to be picked up.
What Halmos Verification does
name: halmos-verification description: Converts structured invariant specifications into compilable Halmos symbolic test suites (.t.sol) that run inside Foundry. Consumes output from the invariant-writer agent. Produces Solidity symbolic tests using halmos-cheatcodes (svm.createUint256, svm.createAddress, etc.) with check_ prefix functions that exhaustively verify properties over all possible inputs. Covers multi-path attack vectors, cross-function composability, arithmetic safety, access co
Alternatives in Testing & QA
- Skill Creator — Generate spec-compliant skills for the cc-polymath library 131 ★
- Forge Speccer — Writes specifications with R-numbered requirements and testable acceptance criteria from brainstorm output 55 ★
- Feature Implementer — Implement a ReviewFlow feature via TDD inside-out 42 ★
Full documentation available on GitHub
View Source RepositoryRelated Agents
Certora Verification
Converts structured invariant specifications into Certora CVL .spec and .conf files. Handles compilation, Pyth
Design Extractor
Extracts precise design specifications from Paper/Figma/Stitch MCPs or local reference images; produces struct
Load Test Generator
Use this agent to generate K6 load test scripts from markdown specs. Converts natural language load test speci
06 Release Readiness.Agent
Release gate decision agent. Consumes all QA pipeline outputs (plan, execution results, defect triage, metrics
Stamity Implementer
Builds one planned unit — code plus the tests that prove it — inside the unit's file set, runs the local gates
Npl PRD Editor
Transforms user stories and feature requests into well-structured PRD documents under project-management/PRDs/
Related Skills
Raze
MCP-first security orchestrator for Solidity smart contracts. Validates AI attack hypotheses, generates Foundr
Supra Dex V3
Uniswap V3 style DEX forked and adapted for Supra MultiVM EVM — built end-to-end in 45 mins using the supra-so
Phase 2 Execution Plan
Phase 2 Execution Plan: Consumes/Produces Pattern (22 Skills)