Summary

Add an <McpServer> algebraic effect that allows Vera programs to expose tools to LLMs via the Model Context Protocol, with contracts guaranteeing tool schema compliance at compile time.

Motivation

This is arguably the flagship use case for Vera as a verified LLM orchestration language. An MCP server exposes typed tools that LLMs can invoke. Vera's contract system can verify at compile time that:

• Tool input parameters match their declared JSON Schema
• Tool outputs conform to expected types
• Preconditions on tool invocation are satisfied
• Side effects are declared and tracked

No other language in the MCP ecosystem offers this level of static verification for tool implementations.

Design

MCP tool dispatch maps naturally to Vera's effect handler pattern — each tool is an effect operation:

effect McpServer {
  op on_tool_call(McpToolRequest -> McpToolResponse);
  op list_tools(Unit -> Array<McpToolSchema>);
}

handle[McpServer] {
  on_tool_call(@McpToolRequest) -> {
    match tool_name(@McpToolRequest.0) {
      "get_weather" -> resume(weather_handler(@McpToolRequest.0)),
      "search" -> resume(search_handler(@McpToolRequest.0)),
      _ -> resume(error_response("Unknown tool")),
    }
  },
  list_tools(@Unit) -> {
    resume(registered_tools)
  }
} in {
  serve_mcp(3000)
}

Dependencies

• JSON standard library type #58 — JSON type (MCP protocol uses JSON-RPC)
• <HttpServer> effect — verified HTTP request handling #305 — HTTP Server effect (MCP runs over HTTP/SSE or stdio)

Implementation notes

• MCP uses JSON-RPC 2.0 over HTTP+SSE or stdio transport
• Tool schemas are JSON Schema — the contract system can verify compliance
• The <Inference> effect (LLM inference effect (<Inference>) #61) composes naturally: a tool handler that calls an LLM would have effects(<McpServer, Inference>)
• Stdio transport could work without HTTP Server (simpler initial implementation)