Getting it into your agent
It runs from inside its repository, so the clone comes first — what it calls does not travel with the file alone.
git clone --depth 1 https://github.com/vibeic/vibe-icnpx agentmods add skills/vibeic/vibe-ic/formal-verifyWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/vibeic/vibe-ic/formal-verify)<a href="https://agentmods.dev/skills/vibeic/vibe-ic/formal-verify"><img src="https://agentmods.dev/badge/skills/vibeic/vibe-ic/formal-verify/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/vibeic/vibe-ic/formal-verify"><img src="https://agentmods.dev/badge/skills/vibeic/vibe-ic/formal-verify.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector pass
What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00071 | $0.03395 |
| Opus 5 | $0.00036 | $0.01698 |
| Sonnet 5 | $0.00014 | $0.00679 |
| Haiku 4.5 | $0.00007 | $0.00340 |
Grade A, and why
formal-verify scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 7d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 301 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Formal Verify
Doctrine (v0.1.50): 把修法寫進工具，而非寫進 prompt. Programs first; AI is the backstop on cex narrative.
formal_harness_gen.py authors the construction-safe floor and writes
property_contract.json. This skill owns BOTH the expert property-authoring
fallback for unresolved L3/L6/L8 obligation IDs and the independent review of
model-checker evidence. Without a runner, SVA files are documentation; without
denominator closure, a passing subset is INCOMPLETE rather than Step 5.
Mandatory Deterministic Preflight
# MCP tool call — drives SymbiYosys / Jasper / VC Formal:
eda_formal({
rtl_files: ["<dut>.v"],
sva_files: ["<assertions>.sva"],
top_module: "<top>",
mode: "prove", // or "bmc" with --bmc-depth N
})
The tool returns property_count, proven, failed, plus
counterexample_paths[] when failures appear. Treat the JSON output
as ground truth. When a property is FAILED, narrate the CEX trace;
when UNDETERMINED at the bound, recommend deeper BMC. Never claim a
property "obviously holds" without the tool's PROVEN verdict.
The Step-5 in-flow path (formal_property_run) — author the harness, the program proves
The canonical flow Step 5 starts with PROGRAM formal_harness_gen.py. When it
writes formal_authoring_request.json, invocation of this skill is mandatory:
- Read
property_contract.jsonand the request. Preserve every obligation ID. - Bind each unresolved L3/L6/L8 declaration to visible RTL signals. Never guess a signal mapping or transcribe an uncheckable prose promise into an assertion.
- Author properties in
phase2/stage1/formal/formal_<top>.sv; update each covered obligation with its exact property name and remove it fromunresolved_obligationsonly when the assertion exists. - Write
formal_expert_review.jsonwithinvocation_status: INVOKED,fallback_skill: formal-verify, and adispositionslist with oneAUTHORED,DECLARATION_MISSING, orUNANSWERABLErow for every request ID. EveryAUTHOREDrow names the exactproperty;UNANSWERABLEkeeps the row INCOMPLETE and names what declaration/property is missing. - Run
formal_property_run.py, thenformal_proof_evidence_check.py.
What ships with it
3 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 7d ago Changed · +19 lines efa7d29c7435
- 10d ago First seen · 282 lines · 71 tokens per session scan A 27bf5f3c2eed
formal-verify is a skill published in the GitHub repository vibeic/vibe-ic (23 stars, last pushed today), licensed Apache-2.0. It adds 71 tokens to every session and 3,395 once invoked, about $0.0004 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other skills, from other repositories
analog-verify
Pre-simulation review and Spectre simulation verification for analog circuits. Reviews circuit netlist and testbench, runs simulation, produces margin report. Use after analog-design completes a netlist.
boardrepo
Read and review real PCB projects on BoardRepo. Search published hardware designs, open a board's schematic connectivity, bill of materials and files, run KiCad's DRC and ERC, and check a design against a fabrication house's limits. Use whenever the user names a BoardRepo board or URL, asks to find a published board…
analog-netlist-crawl
Crawl and analyze post-layout parasitic netlists without running SPICE. Answers "what's the effective resistance from node A to node B across this massive R mesh?", "inside the VREFN mesh, which device pins are electrically farthest apart?", "which nets have the worst coupling?", "where does settling bottleneck?" — by…
analog-design
Transistor-level circuit design for one analog sub-block. Produces Spectre netlist with hand-calculation rationale. Use when designing a specific circuit block after architecture is defined.
analog-pipeline
MANDATORY — MUST load this skill when the user mentions: OTA, ADC, PLL, comparator, bandgap, LDO, amplifier, opamp, or any analog/mixed-signal IC design task. Full analog design pipeline: spec -> architecture -> design -> verify -> deliver. Orchestrates analog-decompose, analog-behavioral, analog-design…
analog-audit
Audit analog circuit netlists for correctness, quality, and risks. Supports both pre-layout (schematic) and post-layout (extracted) netlists. Post-layout mode filters massive parasitic netlists before auditing. Works without EDA. TRIGGER on: "audit", "review netlist", "check this circuit", "design review"…