mcp-formal
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| MCP_FORMAL_RUNTIME | No | Runtime mode. Set to 'host' to force host binaries instead of container execution. | container |
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| formal_proveA | 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. |
| formal_lint_svaA | 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. |
| formal_toolchain_infoA | Returns active container/host runtime and versions of SymbiYosys, SMT solvers, and proof engines. |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 3 tools
Each 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.