End-to-end Model Context Protocol (MCP) servers for verifiers

We describe an end-to-end architecture for Model ContextProtocol (MCP) servers for verifiers and implement this approach forthe Isabelle verifier as a library. The end-to-end approach allows usto develop and execute MCP tools – interactions between the LargeLanguage Model (LLM) and the verifier – in the verifier itself. As a result,we allow the LLM to interact directly with the verifier semantics, notjust the verifier syntax. Moreover – when executed in the verifier – thetools become independent of the MCP server implementation and can bemoved between different end-to-end MCP server implementations for thesame verifier. We showcase our approach by developing example MCPtools that leverage access to the verifier semantics and executing them intwo different end-to-end MCP servers for the Isabelle verifier.