Click on "Install Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@mcp-formal prove the assertions in counter.sv with top module counter using BMC depth 20"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
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 z3engine (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.
// Tool Call: formal_toolchain_info
{
"runtime": "podman",
"image": "localhost/zesun33/asic",
"solvers": ["z3 (Z3 version 5.1.0 - 64 bit)"],
"engines": ["smtbmc_z3"]
}// 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": []
}// 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 }
]
}// 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 ..."]
}Related MCP server: EDA Tools MCP Server
Tool | Parameters | Engine | Description |
|
| SBY | Proves embedded assertions; honest 5-state verdict with counterexample locations. Pass |
|
| Yosys elaboration | Catches SVA syntax/elaboration errors with file:line diagnostics. Proves nothing. |
| none | Probe | SBY version, SMT solvers, and proof engines. |
mcp-formal runs inside the zesun33/asic rootless Podman image (localhost/zesun33/asic):
Container mount: -v <workspace>:/workspace:Z -w /workspace
Podman storage option: --storage-opt overlay.ignore_chown_errors=true
SBY work dirs (sby_work_*/) are created under the workspace and removed unless keep_workdir is set
To force host binaries instead of container execution:
export MCP_FORMAL_RUNTIME=hostBecause 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.
Run the full 6-gate verification suite:
# Full verification (with Podman SBY runs)
./scripts/verify.sh
# Fast / CI verification (headless environments)
./scripts/verify.sh --quickApache-2.0 © 2026 Md Zesun Ahmed Mia
Elaborates RTL with embedded SVA in Yosys to catch syntax and elaboration errors before solver time. Reports file:line diagnostics. Does not prove anything; use formal_prove for verdicts.
| Name | Required | Description | Default |
|---|---|---|---|
| cwd | No | Optional working directory. | |
| top_module | Yes | Top module name. | |
| verilog_sources | Yes | RTL files to elaborate. |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral transparency. It discloses that it reports file:line diagnostics and explicitly states it does not prove anything, making the tool's behavior and limitations clear.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is two sentences, front-loaded with the primary verb and purpose, and contains no redundant or extraneous information. It efficiently conveys the tool's function and its relationship to the sibling tool.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description is complete for the tool's complexity: it states what it does, what it outputs (file:line diagnostics), what it does not do (prove), and the context of use (before solver time). No additional context is needed for correct invocation.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The input schema already provides descriptive text for all three parameters (cwd, top_module, verilog_sources), achieving 100% schema coverage. The description does not add extra parameter semantics, so the baseline score of 3 is appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose with a specific verb ('Elaborates RTL with embedded SVA in Yosys') and its scope ('catch syntax and elaboration errors before solver time'). It explicitly distinguishes itself from sibling tool formal_prove by noting it does not prove anything.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides explicit guidance on when to use it (before solver time for syntax/elaboration checks) and when not to use it, directing the agent to formal_prove for verdicts. This directly addresses the alternative tool and the condition for selecting it.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Proves SystemVerilog assertions embedded in RTL with SymbiYosys (smtbmc+z3), bounded (bmc) or inductive (prove). Returns PROVEN, FAILED with counterexample asserts, UNKNOWN, ERROR, or TIMEOUT. Author properties first with rtl_generate_assertion (mcp-rtl-review); a passing lint does not mean properties hold.
| Name | Required | Description | Default |
|---|---|---|---|
| cwd | No | Optional working directory. | |
| mode | No | Bounded check to depth (bmc) or full induction attempt (prove). Default: bmc. | |
| depth | No | Bound depth in [1, 100] (default: 10). Deeper bounds cost solver time. | |
| defines | No | Preprocessor defines for the read step, e.g. ["FORMAL"] to enable `ifdef FORMAL assertion blocks (iverilog cannot parse SVA, so guard solver-only constructs). | |
| timeout_ms | No | Maximum task time in milliseconds (default: 300000). | |
| top_module | Yes | Top module name. | |
| keep_workdir | No | Keep the SBY work directory for trace inspection (default: false). | |
| verilog_sources | Yes | RTL files containing the design and embedded assert properties. |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden and does well by listing return statuses (PROVEN, FAILED, UNKNOWN, ERROR, TIMEOUT) and the two proof modes. It does not detail side effects such as temporary workdir behavior, though the keep_workdir parameter partially covers that.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is compact and well-structured, with no filler. Each sentence contributes essential information about behavior, outputs, or workflow.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description covers the core context: engine, modes, result kinds, and relationship to assertion authoring and linting. A small gap is the lack of explicit guidance on when to choose formal_prove over formal_lint_sva, though the lint caveat implies it.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so the baseline applies. Each parameter already has a meaningful description, including defaults, constraints, and usage hints, so the description adds little beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: proving SystemVerilog assertions in RTL using SymbiYosys with specific modes. It is easy to distinguish from the sibling lint and toolchain-info tools.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It explicitly explains bounded vs. inductive modes, directs users to author properties with rtl_generate_assertion, and cautions that lint success does not imply proof. This gives strong actionable guidance.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Returns active container/host runtime and versions of SymbiYosys, SMT solvers, and proof engines.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
The description indicates a read-only informational behavior by stating it 'returns' runtime and version data. It does not explicitly mention side effects, but the nature of the tool makes it clear it does not modify state.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single concise sentence that directly states the tool's purpose without unnecessary detail or repetition.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a simple informational tool with no parameters and no output schema, the description fully covers what is returned and is sufficient for an agent to understand its purpose.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool has zero parameters and the input schema is empty, so no parameter-level description is needed. The baseline for zero parameters is 4.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool returns active container/host runtime and versions of SymbiYosys, SMT solvers, and proof engines. It is specific and easily distinguished from the sibling formal verification tools.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies informational use, but it does not explicitly state when to use this tool versus the sibling tools or mention any conditions or alternatives. Usage context is only implied by the nature of the returned data.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections. Dates show when Glama detected each change.
v0.1.0formal_lint_svaformal_proveformal_toolchain_infoEach tool has a clearly distinct purpose: formal_prove runs proofs, formal_lint_sva checks syntax/elaboration, and formal_toolchain_info reports environment details. No overlap or ambiguity exists even without reading full descriptions.
All tools share the formal_ prefix and use snake_case, but formal_prove and formal_lint_sva are verb-oriented while formal_toolchain_info is noun-oriented. This is a minor inconsistency rather than a serious naming problem.
Three tools is a compact, focused set that covers the core formal-verification workflow without redundancy or unnecessary bloat.
The set covers proving, linting/elaboration, and toolchain introspection, which forms a solid lifecycle. A tool for explicitly listing or managing assertions could be missing, but the current coverage is sufficient for typical formal verification tasks.
Unclaimed servers have limited discoverability.
If you are the server author, to access and configure the admin panel.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
Formally-verified injection/exfiltration detector for AI agents (MCP-02).
Pre-execution governance for AI agents. Deterministic PASS/FAIL/REVIEW verdicts, replayable proof.
Preflight QA for AI-agent deliverables with structured verdicts and repair guidance.
We provide all the information about MCP servers via our MCP API.
curl -X GET 'https://glama.ai/api/mcp/v1/servers/zesun33/mcp-formal'
If you have feedback or need assistance with the MCP directory API, please join our Discord server
