@zesun33/mcp-formal

Model Context Protocol (MCP) server for SymbiYosys formal verification (BMC/prove) and SVA linting.

mcp-formal lets AI coding agents and IDEs (Cursor, Windsurf, GitHub Copilot / OpenAI Codex, Claude Code, Google Antigravity, OpenCode, Cline) prove SystemVerilog assertions with SymbiYosys (smtbmc+z3) instead of only simulating them. Author properties first with rtl_generate_assertion (mcp-rtl-review), then prove them here: verdicts are PROVEN, FAILED (with counterexample asserts), UNKNOWN, ERROR, or TIMEOUT — never a silent pass.

Engine reality (verified live): the image ships SBY with the smtbmc z3 engine (z3 5.1.0). The ABC/PDR engine is excluded: it crashes parsing witness output against this Yosys build. Sequential/multi-clock properties may report UNKNOWN or exhaust depth instead of proving; treat those as work for deeper bounds or induction, not as passes.

⚡ Quick Tour: See It in Action

Real Agent Scenarios in 60 Seconds

1. Probing the Toolchain (Zero-Config Verification)

// Tool Call: formal_toolchain_info
{
  "runtime": "podman",
  "image": "ghcr.io/zesun33/asic",
  "solvers": ["z3 (Z3 version 5.1.0 - 64 bit)"],
  "engines": ["smtbmc_z3"]
}

2. Proving a Holding Assertion (Bounded)

// Tool Call: formal_prove {"verilog_sources": ["counter_assert_ok.sv"], "top_module": "cnt_ok", "mode": "bmc", "depth": 6}
{
  "success": true,
  "verdict": "PROVEN",
  "mode": "bmc",
  "depth": 6,
  "failedAssertions": []
}

3. Refuting a False Assertion (Counterexample Triage)

// Tool Call: formal_prove {"verilog_sources": ["counter_assert_bad.sv"], "top_module": "cnt_bad", "mode": "bmc", "depth": 6}
{
  "success": true,
  "verdict": "FAILED",
  "failedAssertions": [
    { "name": "cnt_bad.$assert$counter_assert_bad.sv:14$1", "location": "counter_assert_bad.sv:14", "step": 1 }
  ]
}

4. Catching Syntax Errors Before Solver Time

// Tool Call: formal_lint_sva {"verilog_sources": ["sva_syntax_bad.sv"], "top_module": "sva_broken"}
{
  "success": false,
  "errors": ["sva_syntax_bad.sv:14: syntax error ..."]
}

Tools Exposed

| Tool | Parameters | Engine | Description | | :--- | :--- | :--- | :--- | | formal_prove | verilog_sources: string[], top_module: string, mode?: "bmc" \| "prove", depth?: number [1,100], defines?: string[], keep_workdir?: boolean, cwd?: string | SBY smtbmc z3 | Proves embedded assertions; honest 5-state verdict with counterexample locations. Pass defines: ["FORMAL"] with `ifdef FORMAL-guarded SVA (iverilog cannot parse assertions). | | formal_lint_sva | verilog_sources: string[], top_module: string, cwd?: string | Yosys elaboration | Catches SVA syntax/elaboration errors with file:line diagnostics. Proves nothing. | | formal_toolchain_info | none | Probe | SBY version, SMT solvers, and proof engines. |

Execution Runtime

mcp-formal runs inside the zesun33/asic rootless Podman image so tools are identical on any Linux host.

Public install (recommended — anyone can pull):

podman pull ghcr.io/zesun33/asic:latest
export MCP_FORMAL_IMAGE=ghcr.io/zesun33/asic

ghcr.io/zesun33/asic is the default (anyone can pull). Local builds still work as localhost/zesun33/asic via MCP_FORMAL_IMAGE.

• Container mount: -v <workspace>:/workspace:Z -w /workspace
• Podman storage option: --storage-opt overlay.ignore_chown_errors=true

To force host binaries instead of container execution:

export MCP_FORMAL_RUNTIME=host

Requires SymbiYosys + z3 in the image (shipped in zesun33/asic).

Universal Client & AI IDE Setup

Because mcp-formal implements the standard Model Context Protocol (MCP), it connects seamlessly to any MCP-compliant AI IDE or agent interface:

{
  "mcpServers": {
    "formal": {
      "command": "node",
      "args": ["/path/to/mcp-formal/dist/index.js"]
    }
  }
}

• Cursor: Configure in .cursor/mcp.json.
• Windsurf: Configure in ~/.codeium/windsurf/mcp_config.json.
• GitHub Copilot / OpenAI Codex: Configure via Copilot MCP settings or Codex tool proxy.
• Claude Code: Configure via claude mcp add formal node /path/to/dist/index.js.
• Google Antigravity: Load as workspace MCP server in antigravity.json.
• OpenCode & Cline: Direct stdio JSON-RPC connection.

Verification & Testing

Run the full 6-gate verification suite:

# Full verification (with Podman SBY runs)
./scripts/verify.sh

# Fast / CI verification (headless environments)
./scripts/verify.sh --quick

License

Apache-2.0 © 2026 Md Zesun Ahmed Mia