← All skills
formal-verify
97 / 100 · Low risk
Fine to try.
By vibeic/vibe-ic (GitHub) · design · 32 stars · scanned at commit 17f924c
Run formal property verification (FPV) on RTL by driving model-checkers such as SymbiYosys, Jasper, or VC Formal. Use when the user says "prove this", "formal verify", "model check", "run sby", or has SVA properties from assertion-gen that need to be proven or bounded.
Works with any agent that supports SKILL.md skills.
What this skill can do
Runs commands on your computer
This is disclosed by the author in the skill's SKILL.md or README.
Found in 25 places.
Show 17 more
- vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/bootstrap.mjs, line 181
const res = spawnSync( - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/container_runtime.mjs, line 2
import { spawnSync } from "node:child_process"; - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/devices/_registry.js, line 77
import { spawn, execSync } from "child_process"; - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/devices/_registry.js, line 430
return execSync("id -nG", { stdio: ["ignore", "pipe", "ignore"] }) - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/devices/_registry.js, line 485
const out = execSync( - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/devices/_registry.js, line 486
`docker exec ${container} sh -c 'command -v ${binName}'`, - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 25
import { execSync } from "child_process"; - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 259
const jtagOut = execSync( - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 853
out = execSync(dp.probe, { timeout: 8000, encoding: "utf-8", stdio: ["ignore", "pipe", "pipe"] }).trim(); - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 2090
const { execSync } = await import("child_process"); - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 2170
import { execSync as _execSync } from "child_process"; - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 2254
const { execSync } = await import("child_process"); - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 2433
const { execFileSync } = require("child_process"); - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/index.js, line 2457
output = execFileSync("python3", [program, ...args], { - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/temp_paths.mjs, line 1
import { execFileSync } from "node:child_process"; - vibe-ic-marketplace/plugins/vibe-ic/mcp-eda/src/temp_paths.mjs, line 10
return execFileSync("python3", [helper, ...args], { - vibe-ic-marketplace/plugins/vibe-ic/programs/vibeic_temp.py, line 440
return subprocess.run(argv, env=dict(os.environ)).returncode
and 5 more places
Install
Paste this into your terminal. It downloads exactly the version we scanned, not whatever is newest.
if [ -e ~/.agents/skills/'formal-verify' ] || [ -L ~/.agents/skills/'formal-verify' ]; then echo 'A skill folder named formal-verify already exists — not replacing it' >&2; false; else d=$(mktemp -d) && git clone --quiet --filter=blob:none --no-checkout 'https://github.com/vibeic/vibe-ic' "$d" && git -C "$d" checkout --quiet '17f924c733a532d0b214eee8375d3c74effa1218' -- 'vibe-ic-marketplace/plugins/vibe-ic/skills/formal-verify' && mkdir -p ~/.agents/skills && cp -R "$d"/'vibe-ic-marketplace/plugins/vibe-ic/skills/formal-verify' ~/.agents/skills/'formal-verify' && rm -rf "$d"; fi
Codex reads ~/.agents/skills directly. For Claude Code, Cursor, Copilot, Gemini CLI, Antigravity or OpenCode, also link it. For Claude Code: ln -s ~/.agents/skills/'formal-verify' ~/.claude/skills/'formal-verify' (other agents: ~/.cursor/skills, ~/.copilot/skills, ~/.gemini/skills, ~/.gemini/config/skills, ~/.config/opencode/skills). Or install through the finder skill, which does both.
Badge for your README
The badge for vibeic/vibe-ic shows the score of its lowest-scoring skill.
[](https://zalavijaysinh.github.io/skilltrust/repos/vibeic/vibe-ic/)
Score history
| Date | Version | Score |
|---|
| 2026-11-12 | 17f924c | 97 |