Skill

gf-formal

Generates SVA properties from natural language, configures SymbiYosys, runs formal proofs on hardware designs like FIFOs, and explains pass/fail results.

testing

code-quality

npx claudepluginhub codejunkie99/gateflow-plugin --plugin gateflow

Tool Access

This skill is limited to using the following tools:

BashReadWriteGlobGrepTask

Preview

```bash

SKILL.md

Similar Skills

design-system

167.4k

Generates design tokens/docs from CSS/Tailwind/styled-components codebases, audits visual consistency across 10 dimensions, detects AI slop in UI.

team-skills-platform

ui-demo

167.4k

Records polished WebM UI demo videos of web apps using Playwright with cursor overlay, natural pacing, and three-phase scripting. Activates for demo, walkthrough, screen recording, or tutorial requests.

team-skills-platform

kotlin-patterns

167.4k

Delivers idiomatic Kotlin patterns for null safety, immutability, sealed classes, coroutines, Flows, extensions, DSL builders, and Gradle DSL. Use when writing, reviewing, refactoring, or designing Kotlin code.

team-skills-platform

Stats

Parent Repo Stars39

Parent Repo Forks5

Last CommitMar 26, 2026

Actions

View Source View Plugin View on GitHub View README

GF-Formal — Formal Verification Skill

Tool Detection

which sby

If not found:

---GATEFLOW-RESULT---
STATUS: ERROR
DETAILS: SymbiYosys not installed. Install to enable formal verification.
  pip install symbiyosys
  Also need: yosys, z3 (or yices2)
  macOS: brew install yosys z3
  Linux: sudo apt install yosys z3
---END-GATEFLOW-RESULT---

Workflow

Parse request — What properties to verify? Which module?
Read the design — Understand ports, signals, behavior
Spawn sv-formal agent — Generate properties + .sby config
Run SymbiYosys: sby -f <config>.sby
Parse results — Read sby output for pass/fail/counterexample
Report — 3-layer error translation if failed, clear summary if passed

Result Format

---GATEFLOW-RESULT---
STATUS: PASS | FAIL | ERROR
PROOFS: N proved, M failed, K covers
FILES: [generated files]
DETAILS: [proof results or counterexample explanation]
---END-GATEFLOW-RESULT---

Integration with /gf Orchestrator

Formal verification is an optional enhancement step:

After simulation passes, for safety-critical designs
When user explicitly requests formal verification
For CDC, FIFO, or protocol designs