formal-verify SKILL.md skillA
formal-verify from vibeic/vibe-ic is an agent skill: a SKILL.md folder an AI agent loads when a task calls for it.
mdr add vibeic/vibe-ic/formal-verify@git:20261108.1472dd9Pins git:20261108.1472dd9 in mdr.lock. Pin the fingerprint instead.
- Audit grade
- A, 17 of 17 checks passed
- Kind
- SKILL.md skill
- Repository
- vibeic/vibe-ic
- Path
vibe-ic-marketplace/plugins/vibe-ic/skills/formal-verify/SKILL.md- Versions recorded
- 9
- Latest version
- git:20261108.1472dd9, committed Nov 8, 2026
- First version recorded
- Jun 13, 2026
- Size
- 12,889 bytes
- Repository stars
- 32
- License
- Apache-2.0
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.
Collected from public GitHub. Every version is saved exactly as it was and never changes. Install it at an exact version with the mdr tool, and every file is checked before it reaches your agent. The main file is checked against the SHA-256 fingerprint recorded here, and the others against the fingerprints GitHub keeps for its source commit. The automatic checks below grade the latest version, and the same checks always give the same file the same grade.
What the file says
# 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
```bash
# 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
…Read the whole file at its exact version.
How to install
mdr add vibeic/vibe-ic/formal-verify@sha256:9422b5e4a2852e7fThe line at the top of this page pins the label git:20261108.1472dd9, which is what most people want. This one pins the sha256 fingerprint of the contents instead, so it survives a label being moved. Either way the exact version is written to mdr.lock, and mdr install downloads and checks those contents again, so it installs them exactly or stops with an error.
[](https://markdownregistry.com/a/art_lsqxsumjmfftevsb)
4 badge image fetches in 30 days. What the badge shows.
Versions
The registry has recorded 9 versions of this file, between Jun 13, 2026 and Nov 8, 2026, about one every 18 days.
| version | committed | commit | size | audit | |
|---|---|---|---|---|---|
| git:20261108.1472dd9 latest | 2026-11-08 | 1472dd9 | 12,889 B | A | view · diff |
| git:20261106.a0a79f8 | 2026-11-06 | a0a79f8 | 12,105 B | A | view · diff |
| git:20261105.13b7a3f | 2026-11-05 | 13b7a3f | 12,824 B | A | view · diff |
| git:20260929.55161de | 2026-09-29 | 55161de | 13,492 B | A | view · diff |
| git:20260901.2a9d213 | 2026-09-01 | 2a9d213 | 13,114 B | A | view · diff |
| git:20260721.351ba31 | 2026-07-21 | 351ba31 | 11,859 B | A | view · diff |
| git:20260721.93aab52 | 2026-07-21 | 93aab52 | 11,859 B | A | view · diff |
| git:20260713.6d70fab | 2026-07-13 | 6d70fab | 10,166 B | A | view · diff |
| git:20260613.86cacb4 | 2026-06-13 | 86cacb4 | 8,155 B | A | view |
Audit of the latest version
- pass: Frontmatter block present
- pass: Frontmatter declares a name
- pass: Frontmatter declares a description
- pass: Size between 200 bytes and 200 KB (12889 bytes)
- pass: No zero-width or bidi control characters
- pass: No instruction hidden inside an HTML comment
- pass: No link to an exfiltration or paste host
- pass: No credential-shaped string
- pass: No instruction to send local credentials anywhere
- pass: No text hidden with inline styles
- pass: No prompt-injection phrasing
- pass: No curl or wget piped into a shell
- pass: No recursive delete of root, home or parent
- pass: No instruction to read or print local credentials
- pass: No base64 blob over 200 characters
- pass: No link to a raw IP address
- pass: No script tag
Source
vibeic/vibe-ic · 32 stars · license Apache-2.0 · pushed 2026-11-08 · branch main
API
GET https://markdownregistry.com/api/v1/artifacts/art_lsqxsumjmfftevsb GET https://markdownregistry.com/api/v1/resolve?ref=vibeic/vibe-ic/formal-verify GET https://markdownregistry.com/api/v1/blob/9422b5e4a2852e7f232e30705fc13cc16b9fc9fc99e450d84f855add72af2705
Your AI assistant does the legwork. You hear about the deals worth your word. Hand yours the standing instructions at modelranch.com and it joins the network that reads files like this one.
Guides: the SKILL.md format and its required fields · what to check before you install a skill · how to pin a skill to an exact version · where to find agent skills · keeping a team on the same skills · which agent file does what.