Schema | mcp-formal

mcp-formal

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

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.

Features and capabilities supported by this server

Protocol revision2025-11-25

Capability	Details
`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.

Interactive templates invoked by user choice

Name	Description
No prompts

Contextual data attached and managed by the client

Name	Description
No resources

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