diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..6bcc45d
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,50 @@
+name: CI
+
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+    branches: [main, master]
+
+jobs:
+  build-and-test:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Install Nix
+        uses: DeterminateSystems/nix-installer-action@main
+        with:
+          extra-conf: |
+            experimental-features = nix-command flakes
+
+      - name: Setup Nix cache
+        uses: DeterminateSystems/magic-nix-cache-action@main
+
+      - name: Build project
+        run: nix build .#agda-mcp
+
+      - name: Run tests
+        run: nix build .#checks.x86_64-linux.agda-mcp-tests --print-build-logs
+
+  # Optional: Check that flake evaluates correctly
+  flake-check:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Install Nix
+        uses: DeterminateSystems/nix-installer-action@main
+        with:
+          extra-conf: |
+            experimental-features = nix-command flakes
+
+      - name: Setup Nix cache
+        uses: DeterminateSystems/magic-nix-cache-action@main
+
+      - name: Check flake
+        run: nix flake check
diff --git a/Main.hs b/Main.hs
index b3e8a53..b1c30aa 100644
--- a/Main.hs
+++ b/Main.hs
@@ -1,48 +1,455 @@
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# OPTIONS_GHC -Wno-name-shadowing #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 
 module Main where
 
-import MCP.Server
-import MCP.Server.Derive
+import Control.Monad.IO.Class (liftIO)
+import Data.Aeson (Value, toJSON)
+import qualified Data.Aeson as JSON
+import Data.IORef
+import qualified Data.Map.Strict as Map
+import Data.Maybe (fromMaybe)
+import Data.Text (Text)
 import System.IO (hSetEncoding, stderr, stdout, utf8, hPutStrLn)
+import System.IO.Unsafe (unsafePerformIO)
+
+import MCP.Protocol hiding (error)
+import MCP.Server hiding (ServerState)
+import MCP.Server.HTTP
+import MCP.Types
 
 import AgdaMCP.Server
 import AgdaMCP.Types
+import qualified AgdaMCP.SessionManager as SessionManager
+
+-- | Use IORef for global session manager
+{-# NOINLINE globalSessionManagerRef #-}
+globalSessionManagerRef :: IORef (Maybe (SessionManager.SessionManager ServerState))
+globalSessionManagerRef = unsafePerformIO $ newIORef Nothing
+
+setGlobalSessionManager :: SessionManager.SessionManager ServerState -> IO ()
+setGlobalSessionManager mgr = writeIORef globalSessionManagerRef (Just mgr)
+
+getGlobalSessionManager :: IO (SessionManager.SessionManager ServerState)
+getGlobalSessionManager = do
+    mMgr <- readIORef globalSessionManagerRef
+    case mMgr of
+        Just mgr -> return mgr
+        Nothing -> error "Session manager not initialized"
+
+-- | Instance of MCPServer for our Agda MCP Server
+-- We need to use MCPServerM monad for the implementation
+instance MCPServer MCPServerM where
+    handleListTools _params = do
+        let tools = agdaTools
+        return $ ListToolsResult
+            { tools = tools
+            , nextCursor = Nothing
+            , _meta = Nothing
+            }
+
+    handleCallTool CallToolParams{name = toolName, arguments = mArgs} = do
+        result <- liftIO $ do
+            -- Get session manager from global state
+            manager <- getGlobalSessionManager
+            let args = fromMaybe Map.empty mArgs
+            callAgdaTool manager toolName args
+        return result
+
+    -- Resources - use default implementations for now
+    handleListResources _params = do
+        return $ ListResourcesResult
+            { resources = agdaResources
+            , nextCursor = Nothing
+            , _meta = Nothing
+            }
+
+    handleReadResource ReadResourceParams{uri = resourceUri} = do
+        result <- liftIO $ do
+            manager <- getGlobalSessionManager
+            readAgdaResource manager resourceUri
+        return result
+
+    -- Prompts - not implemented yet
+    handleListPrompts _params = return $ ListPromptsResult
+        { prompts = []
+        , nextCursor = Nothing
+        , _meta = Nothing
+        }
+
+    handleGetPrompt _params = return $ GetPromptResult
+        { messages = []
+        , description = Nothing
+        , _meta = Nothing
+        }
+
+    -- Other handlers use defaults
+    handleSetLevel _params = liftIO $ putStrLn "Log level set"
+
+-- | Define the Agda tools list for the MCP protocol
+agdaTools :: [Tool]
+agdaTools =
+    [ mkTool "agda_load" "Load and type-check an Agda file"
+        [("file", "string", "Path to the Agda file", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_get_goals" "List all goals/holes in the currently loaded file"
+        [("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_get_goal_type" "Get the type of a specific goal"
+        [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_get_goal_type_implicits" "Get the type of a specific goal with implicit arguments shown"
+        [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_get_context" "Get the context (available variables and their types) at a goal"
+        [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_get_context_implicits" "Get the context at a goal with implicit arguments shown"
+        [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_give" "Fill a goal/hole with an expression"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("expression", "string", "Agda expression to use", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_refine" "Refine a goal with a constructor or function, introducing new sub-goals"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("expression", "string", "Agda expression to refine with", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_case_split" "Split a goal by pattern matching on a variable"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("variable", "string", "Name of the variable to case-split on", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_compute" "Parse and display an expression in a goal's context"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("expression", "string", "Agda expression to compute", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_infer_type" "Infer the type of an expression in a goal's context"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("expression", "string", "Agda expression to infer type for", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_intro" "Introduce variables using the intro tactic"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_auto" "Attempt automatic proof search to fill a goal"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("timeout", "integer", "Optional timeout in milliseconds", False)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_auto_all" "Attempt automatic proof search on all goals"
+        [("timeout", "integer", "Optional timeout in milliseconds", False)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_solve_one" "Attempt to solve a specific goal using Agda's constraint solver"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_helper_function" "Generate a helper function skeleton for a goal"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("helperName", "string", "Suggested name for the helper function", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_goal_type_context" "Get both the goal type and context together"
+        [("goalId", "integer", "The numeric ID of the goal/hole", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_goal_at_position" "Find which goal exists at a specific file position"
+        [("file", "string", "Path to the Agda file", True)
+        ,("line", "integer", "Line number (1-indexed)", True)
+        ,("column", "integer", "Column number (1-indexed)", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_goto_definition" "Navigate to the definition of a symbol at a specific position"
+        [("file", "string", "Path to the Agda file", True)
+        ,("line", "integer", "Line number (1-indexed)", True)
+        ,("column", "integer", "Column number (1-indexed)", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_search_about" "Search for definitions by name or type signature"
+        [("query", "string", "Search query", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_show_module" "Show the contents of a module"
+        [("moduleName", "string", "Fully qualified module name", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_show_constraints" "Show all unsolved type-checking constraints"
+        [("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_why_in_scope" "Look up documentation and scope information for a name"
+        [("name", "string", "Name to look up", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    , mkTool "agda_list_postulates" "List all postulates in a file"
+        [("file", "string", "Path to the Agda file", True)
+        ,("sessionId", "string", "Optional session ID for multi-agent isolation", False)
+        ,("format", "string", "Response format: Concise (default) or Full", False)
+        ]
+    ]
+
+-- | Helper to create a tool definition
+mkTool :: Text -> Text -> [(Text, Text, Text, Bool)] -> Tool
+mkTool toolName desc params = Tool
+    { name = toolName
+    , title = Nothing
+    , description = Just desc
+    , inputSchema = InputSchema
+        { schemaType = "object"
+        , properties = Just $ Map.fromList
+            [(pName, toJSON $ Map.fromList
+                [ ("type" :: Text, JSON.String pType)
+                , ("description", JSON.String pDesc)
+                ]) | (pName, pType, pDesc, _) <- params]
+        , required = Just [pName | (pName, _, _, True) <- params]
+        }
+    , outputSchema = Nothing
+    , annotations = Nothing
+    , _meta = Nothing
+    }
+
+-- | Define Agda resources
+agdaResources :: [Resource]
+agdaResources =
+    [ Resource
+        { uri = "agda://goals"
+        , name = "goals"
+        , title = Just "Agda Goals"
+        , description = Just "List of all goals in the currently loaded Agda file"
+        , mimeType = Just "application/json"
+        , size = Nothing
+        , annotations = Nothing
+        , _meta = Nothing
+        }
+    , Resource
+        { uri = "agda://file-context"
+        , name = "file-context"
+        , title = Just "File Context"
+        , description = Just "Overall context and scope information for the loaded file"
+        , mimeType = Just "application/json"
+        , size = Nothing
+        , annotations = Nothing
+        , _meta = Nothing
+        }
+    ]
+
+-- | Call an Agda tool based on name and arguments
+callAgdaTool :: SessionManager.SessionManager ServerState -> Text -> Map.Map Text Value -> IO CallToolResult
+callAgdaTool manager toolName args = do
+    -- Parse tool and call handler
+    mTool <- parseAgdaTool toolName args
+    case mTool of
+        Nothing -> return $ CallToolResult
+            { content = [TextContentType $ TextContent "text" ("Unknown tool: " <> toolName) Nothing Nothing]
+            , structuredContent = Nothing
+            , isError = Just True
+            , _meta = Nothing
+            }
+        Just tool -> do
+            result <- handleAgdaToolWithSession manager tool
+            return $ CallToolResult
+                { content = [result]
+                , structuredContent = Nothing
+                , isError = Nothing
+                , _meta = Nothing
+                }
+
+-- | Parse tool name and arguments to AgdaTool
+parseAgdaTool :: Text -> Map.Map Text Value -> IO (Maybe AgdaTool)
+parseAgdaTool toolName args = do
+    let sessionId = getTextArg "sessionId" args
+        format = getTextArg "format" args
+
+    return $ case toolName of
+        "agda_load" -> do
+            file <- getTextArg "file" args
+            Just $ AgdaLoad file sessionId format
+        "agda_get_goals" ->
+            Just $ AgdaGetGoals sessionId format
+        "agda_get_goal_type" -> do
+            goalId <- getIntArg "goalId" args
+            Just $ AgdaGetGoalType goalId sessionId format
+        "agda_get_goal_type_implicits" -> do
+            goalId <- getIntArg "goalId" args
+            Just $ AgdaGetGoalTypeImplicits goalId sessionId format
+        "agda_get_context" -> do
+            goalId <- getIntArg "goalId" args
+            Just $ AgdaGetContext goalId sessionId format
+        "agda_get_context_implicits" -> do
+            goalId <- getIntArg "goalId" args
+            Just $ AgdaGetContextImplicits goalId sessionId format
+        "agda_give" -> do
+            goalId <- getIntArg "goalId" args
+            expression <- getTextArg "expression" args
+            Just $ AgdaGive goalId expression sessionId format
+        "agda_refine" -> do
+            goalId <- getIntArg "goalId" args
+            expression <- getTextArg "expression" args
+            Just $ AgdaRefine goalId expression sessionId format
+        "agda_case_split" -> do
+            goalId <- getIntArg "goalId" args
+            variable <- getTextArg "variable" args
+            Just $ AgdaCaseSplit goalId variable sessionId format
+        "agda_compute" -> do
+            goalId <- getIntArg "goalId" args
+            expression <- getTextArg "expression" args
+            Just $ AgdaCompute goalId expression sessionId format
+        "agda_infer_type" -> do
+            goalId <- getIntArg "goalId" args
+            expression <- getTextArg "expression" args
+            Just $ AgdaInferType goalId expression sessionId format
+        "agda_intro" -> do
+            goalId <- getIntArg "goalId" args
+            Just $ AgdaIntro goalId sessionId format
+        "agda_auto" -> do
+            goalId <- getIntArg "goalId" args
+            let timeout = getIntArg "timeout" args
+            Just $ AgdaAuto goalId timeout sessionId format
+        "agda_auto_all" -> do
+            let timeout = getIntArg "timeout" args
+            Just $ AgdaAutoAll timeout sessionId format
+        "agda_solve_one" -> do
+            goalId <- getIntArg "goalId" args
+            Just $ AgdaSolveOne goalId sessionId format
+        "agda_helper_function" -> do
+            goalId <- getIntArg "goalId" args
+            helperName <- getTextArg "helperName" args
+            Just $ AgdaHelperFunction goalId helperName sessionId format
+        "agda_goal_type_context" -> do
+            goalId <- getIntArg "goalId" args
+            Just $ AgdaGoalTypeContext goalId sessionId format
+        "agda_goal_at_position" -> do
+            file <- getTextArg "file" args
+            line <- getIntArg "line" args
+            column <- getIntArg "column" args
+            Just $ AgdaGoalAtPosition file line column sessionId format
+        "agda_goto_definition" -> do
+            file <- getTextArg "file" args
+            line <- getIntArg "line" args
+            column <- getIntArg "column" args
+            Just $ AgdaGotoDefinition file line column sessionId format
+        "agda_search_about" -> do
+            query <- getTextArg "query" args
+            Just $ AgdaSearchAbout query sessionId format
+        "agda_show_module" -> do
+            moduleName <- getTextArg "moduleName" args
+            Just $ AgdaShowModule moduleName sessionId format
+        "agda_show_constraints" ->
+            Just $ AgdaShowConstraints sessionId format
+        "agda_why_in_scope" -> do
+            nameArg <- getTextArg "name" args
+            Just $ AgdaWhyInScope nameArg sessionId format
+        "agda_list_postulates" -> do
+            file <- getTextArg "file" args
+            Just $ AgdaListPostulates file sessionId format
+        _ -> Nothing
+
+-- | Get a text argument from the map
+getTextArg :: Text -> Map.Map Text Value -> Maybe Text
+getTextArg key args = case Map.lookup key args of
+    Just (JSON.String s) -> Just s
+    _ -> Nothing
+
+-- | Get an integer argument from the map
+getIntArg :: Text -> Map.Map Text Value -> Maybe Int
+getIntArg key args = case Map.lookup key args of
+    Just (JSON.Number n) -> Just (floor n)
+    _ -> Nothing
+
+-- | Read an Agda resource
+readAgdaResource :: SessionManager.SessionManager ServerState -> Text -> IO ReadResourceResult
+readAgdaResource _manager _resourceUri = do
+    -- For now, return empty result - resources need more implementation
+    return $ ReadResourceResult
+        { contents = []
+        , _meta = Nothing
+        }
 
 main :: IO ()
 main = do
-  -- Set UTF-8 encoding for proper Unicode handling
-  hSetEncoding stdout utf8
-  hSetEncoding stderr utf8
-
-  hPutStrLn stderr "Starting Agda MCP Server on http://localhost:3000/mcp"
-  hPutStrLn stderr "Session isolation enabled: pass 'sessionId' parameter for multi-agent support"
-
-  -- Initialize session manager (replaces single server state)
-  sessionManager <- initSessionManager
-
-  -- Define handlers that close over sessionManager
-  let handleTool :: AgdaTool -> IO Content
-      handleTool = handleAgdaToolWithSession sessionManager
-
-      handleResource :: URI -> AgdaResource -> IO ResourceContent
-      handleResource = handleAgdaResourceWithSession sessionManager
-
-      -- Derive MCP handlers using Template Haskell
-      tools = $(deriveToolHandlerWithDescription ''AgdaTool 'handleTool agdaToolDescriptions)
-      resources = $(deriveResourceHandlerWithDescription ''AgdaResource 'handleResource agdaResourceDescriptions)
-
-   in -- Run the MCP server with HTTP transport
-      runMcpServerHttp
-        McpServerInfo
-          { serverName = "Agda MCP Server"
-          , serverVersion = "1.0.0"
-          , serverInstructions = "A Model Context Protocol server for interactive Agda development. Provides tools for loading files, working with goals/holes, refining proofs, and exploring scope. Supports multi-agent isolation via sessionId parameter."
-          }
-        McpServerHandlers
-          { prompts = Nothing  -- No prompts defined yet
-          , resources = Just resources
-          , tools = Just tools
-          }
+    -- Set UTF-8 encoding for proper Unicode handling
+    hSetEncoding stdout utf8
+    hSetEncoding stderr utf8
+
+    hPutStrLn stderr "Starting Agda MCP Server on http://localhost:3000/mcp"
+    hPutStrLn stderr "Session isolation enabled: pass 'sessionId' parameter for multi-agent support"
+
+    -- Initialize session manager
+    sessionManager <- initSessionManager
+    setGlobalSessionManager sessionManager
+
+    let serverInfo = Implementation
+            { name = "Agda MCP Server"
+            , title = Just "Agda MCP Server"
+            , version = "1.0.0"
+            }
+
+    let resourcesCap = ResourcesCapability
+            { subscribe = Just False
+            , listChanged = Just False
+            }
+    let promptsCap = PromptsCapability
+            { listChanged = Just False
+            }
+    let toolsCap = ToolsCapability
+            { listChanged = Just False
+            }
+
+    let capabilities = ServerCapabilities
+            { resources = Just resourcesCap
+            , prompts = Just promptsCap
+            , tools = Just toolsCap
+            , completions = Nothing
+            , logging = Nothing
+            , experimental = Nothing
+            }
+
+    let config = HTTPServerConfig
+            { httpPort = 3000
+            , httpBaseUrl = "http://localhost:3000"
+            , httpServerInfo = serverInfo
+            , httpCapabilities = capabilities
+            , httpEnableLogging = True
+            , httpOAuthConfig = Nothing
+            , httpJWK = Nothing
+            , httpProtocolVersion = mcpProtocolVersion
+            }
+
+    runServerHTTP config
diff --git a/agda-mcp.cabal b/agda-mcp.cabal
index 2572e63..816b6c4 100644
--- a/agda-mcp.cabal
+++ b/agda-mcp.cabal
@@ -9,6 +9,13 @@ author: Claude Code
 maintainer: claude-code@anthropic.com
 category: Development
 build-type: Simple
+extra-source-files:
+  test/*.agda
+  test/edit-persistence/*.agda
+data-dir: test
+data-files:
+  *.agda
+  edit-persistence/*.agda
 
 library
   exposed-modules:
@@ -30,7 +37,8 @@ library
     directory >= 1.3,
     bytestring >= 0.10,
     vector >= 0.12,
-    mcp-server >= 0.1.0.15,
+    mcp >= 0.3.0.0,
+    data-default >= 0.7,
     unordered-containers >= 0.2,
     uuid >= 1.3,
     stm >= 2.5,
@@ -49,7 +57,11 @@ executable agda-mcp
   build-depends:
     base >= 4.14 && < 5,
     agda-mcp,
-    mcp-server >= 0.1.0.15
+    mcp >= 0.3.0.0,
+    data-default >= 0.7,
+    text >= 1.2,
+    aeson >= 2.0,
+    containers >= 0.6
   default-language: Haskell2010
   default-extensions:
     OverloadedStrings
@@ -64,6 +76,9 @@ test-suite agda-mcp-tests
     AgdaMCP.MultiAgentSpec
     AgdaMCP.EditPersistenceSpec
     AgdaMCP.TestUtils
+    Paths_agda_mcp
+  autogen-modules:
+    Paths_agda_mcp
   build-depends:
     base >= 4.14 && < 5,
     agda-mcp,
@@ -75,7 +90,8 @@ test-suite agda-mcp-tests
     vector >= 0.12,
     filepath >= 1.4,
     directory >= 1.3,
-    mcp-server >= 0.1.0.15,
+    mcp >= 0.3.0.0,
+    containers >= 0.6,
     async >= 2.2,
     random >= 1.2
   hs-source-dirs: test
diff --git a/flake.lock b/flake.lock
index 81ebfff..f25eef4 100644
--- a/flake.lock
+++ b/flake.lock
@@ -33,19 +33,19 @@
         "type": "github"
       }
     },
-    "mcp-server-hs": {
+    "mcp": {
       "flake": false,
       "locked": {
-        "lastModified": 1755071752,
-        "narHash": "sha256-DaSefoJKo6AJ9Gd8gwalVkkd5P7MVnstdeL6LV2izvY=",
-        "owner": "drshade",
-        "repo": "haskell-mcp-server",
-        "rev": "92c70a93446adca0c7cfced97a93eed23bfb5200",
+        "lastModified": 1753988023,
+        "narHash": "sha256-gTV52O4chiB8ehw/nNFvX5cYXACswrqE7aPA+5w/61g=",
+        "owner": "Tritlo",
+        "repo": "mcp",
+        "rev": "5ef0860698e0e2beecad7ea7d64bba53efca8034",
         "type": "github"
       },
       "original": {
-        "owner": "drshade",
-        "repo": "haskell-mcp-server",
+        "owner": "Tritlo",
+        "repo": "mcp",
         "type": "github"
       }
     },
@@ -84,7 +84,7 @@
       "inputs": {
         "flake-parts": "flake-parts",
         "haskell-flake": "haskell-flake",
-        "mcp-server-hs": "mcp-server-hs",
+        "mcp": "mcp",
         "nixpkgs": "nixpkgs"
       }
     }
diff --git a/flake.nix b/flake.nix
index 13bfe5a..cd163d5 100644
--- a/flake.nix
+++ b/flake.nix
@@ -3,7 +3,7 @@
     nixpkgs.url = "github:nixos/nixpkgs/e643668fd71b949c53f8626614b21ff71a07379d";
     flake-parts.url = "github:hercules-ci/flake-parts";
     haskell-flake.url = "github:srid/haskell-flake";
-    mcp-server-hs = { url = "github:drshade/haskell-mcp-server"; flake = false; };
+    mcp = { url = "github:Tritlo/mcp"; flake = false; };
   };
   outputs = inputs@{ self, nixpkgs, flake-parts, ... }:
     flake-parts.lib.mkFlake { inherit inputs; } {
@@ -26,15 +26,12 @@
           # (defined by `defaults.packages` option).
           #
           packages = {
-            mcp-server.source = pkgs.applyPatches {
-              name = "mcp-server-patched";
-              src = inputs.mcp-server-hs;
-              patches = [ ./patches/mcp-server-header-optional.patch ];
-            };
+            mcp.source = inputs.mcp;
             # aeson.source = "1.5.0.0";      # Override aeson to a custom version from Hackage
             # shower.source = inputs.shower; # Override shower to a custom source path
           };
           settings = {
+            mcp.jailbreak = true;
             #  aeson = {
             #    check = false;
             #  };
@@ -61,7 +58,7 @@
         };
 
         # haskell-flake doesn't set the default package, but you can do it here.
-        packages.default = self'.packages.example;
+        packages.default = self'.packages.agda-mcp;
       };
     };
 }
diff --git a/src/AgdaMCP/FileEdit.hs b/src/AgdaMCP/FileEdit.hs
index 82accd1..f0eb8bd 100644
--- a/src/AgdaMCP/FileEdit.hs
+++ b/src/AgdaMCP/FileEdit.hs
@@ -139,23 +139,25 @@ applyReplaceLine file lineNum clauses _indentLevel _needsReload = do
     then putStrLn $ "Warning: Line number " ++ show lineNum ++ " out of bounds"
     else do
       -- Split at line position
-      let (beforeLines, originalLine:afterLines) = splitAt (lineNum - 1) lines'
-
-      -- Calculate indentation from the original line (leading whitespace)
-      let originalIndent = T.takeWhile (== ' ') originalLine
-      let indentLevel = T.length originalIndent
-
-      -- Apply the same indentation to each clause
-      -- Note: Agda provides clauses without leading whitespace
-      let indentedClauses = map (originalIndent <>) clauses
-
-      -- Reconstruct file
-      let newContent = T.unlines $ beforeLines ++ indentedClauses ++ afterLines
-      TIO.writeFile file newContent
-
-      putStrLn $ "Replaced line " ++ show lineNum ++ " with " ++
-                 show (length clauses) ++ " clauses (indent level: " ++
-                 show indentLevel ++ ")"
+      let (beforeLines, rest) = splitAt (lineNum - 1) lines'
+      case rest of
+        [] -> putStrLn $ "Warning: Line number " ++ show lineNum ++ " resulted in empty rest"
+        (originalLine:afterLines) -> do
+          -- Calculate indentation from the original line (leading whitespace)
+          let originalIndent = T.takeWhile (== ' ') originalLine
+          let indentLevel = T.length originalIndent
+
+          -- Apply the same indentation to each clause
+          -- Note: Agda provides clauses without leading whitespace
+          let indentedClauses = map (originalIndent <>) clauses
+
+          -- Reconstruct file
+          let newContent = T.unlines $ beforeLines ++ indentedClauses ++ afterLines
+          TIO.writeFile file newContent
+
+          putStrLn $ "Replaced line " ++ show lineNum ++ " with " ++
+                     show (length clauses) ++ " clauses (indent level: " ++
+                     show indentLevel ++ ")"
 
 -- ============================================================================
 -- Strategy 3: BatchEdits (reverse-order application)
diff --git a/src/AgdaMCP/Server.hs b/src/AgdaMCP/Server.hs
index 3ded240..8884a5a 100644
--- a/src/AgdaMCP/Server.hs
+++ b/src/AgdaMCP/Server.hs
@@ -42,7 +42,7 @@ import System.FilePath (takeDirectory)
 import System.Directory (listDirectory)
 
 -- MCP Server library
-import qualified MCP.Server
+import MCP.Types (Content, ContentBlock(..), TextContent(..), TextResourceContents(..), ResourceContents(..))
 import qualified AgdaMCP.Types
 import qualified AgdaMCP.Repl as Repl
 import qualified AgdaMCP.SessionManager as SessionManager
@@ -884,9 +884,13 @@ initServerState = do
   putStrLn "Persistent REPL started"
   pure stateRef
 
+-- | Helper to create a text content response
+mkTextContent :: Text -> Content
+mkTextContent txt = TextContentType $ TextContent "text" txt Nothing Nothing
+
 -- MCP Tool Handler - routes commands through persistent REPL
 -- This will be called by the mcp-server library when a tool is invoked
-handleAgdaTool :: IORef ServerState -> AgdaMCP.Types.AgdaTool -> IO MCP.Server.Content
+handleAgdaTool :: IORef ServerState -> AgdaMCP.Types.AgdaTool -> IO Content
 handleAgdaTool stateRef tool = do
   -- Special handling for tools that need custom logic (don't use REPL)
   case tool of
@@ -894,34 +898,34 @@ handleAgdaTool stateRef tool = do
       -- Run directly in TCM (not through REPL)
       result <- runTCMTop $ mcpListPostulates stateRef (T.unpack file)
       case result of
-        Left err -> pure $ MCP.Server.ContentText $ "Error: " <> T.pack (show err)
+        Left err -> pure $ mkTextContent $ "Error: " <> T.pack (show err)
         Right (AgdaResult _ _ (Just val)) -> do
           let responseFormat = Format.getFormat tool
           let responseText = Format.formatResponse responseFormat val
-          pure $ MCP.Server.ContentText responseText
-        Right _ -> pure $ MCP.Server.ContentText "No postulates found"
+          pure $ mkTextContent responseText
+        Right _ -> pure $ mkTextContent "No postulates found"
 
     AgdaMCP.Types.AgdaGoalAtPosition{file, line, column} -> do
       -- Run directly in TCM to find goal at position
       result <- runTCMTop $ mcpGoalAtPosition stateRef (T.unpack file) line column
       case result of
-        Left err -> pure $ MCP.Server.ContentText $ "Error: " <> T.pack (show err)
+        Left err -> pure $ mkTextContent $ "Error: " <> T.pack (show err)
         Right (AgdaResult _ _ (Just val)) -> do
           let responseFormat = Format.getFormat tool
           let responseText = Format.formatResponse responseFormat val
-          pure $ MCP.Server.ContentText responseText
-        Right (AgdaResult _ msg Nothing) -> pure $ MCP.Server.ContentText msg
+          pure $ mkTextContent responseText
+        Right (AgdaResult _ msg Nothing) -> pure $ mkTextContent msg
 
     AgdaMCP.Types.AgdaGotoDefinition{file, line, column} -> do
       -- Run directly in TCM to find definition at position
       result <- runTCMTop $ mcpGotoDefinition stateRef (T.unpack file) line column
       case result of
-        Left err -> pure $ MCP.Server.ContentText $ "Error: " <> T.pack (show err)
+        Left err -> pure $ mkTextContent $ "Error: " <> T.pack (show err)
         Right (AgdaResult _ _ (Just val)) -> do
           let responseFormat = Format.getFormat tool
           let responseText = Format.formatResponse responseFormat val
-          pure $ MCP.Server.ContentText responseText
-        Right (AgdaResult _ msg Nothing) -> pure $ MCP.Server.ContentText msg
+          pure $ mkTextContent responseText
+        Right (AgdaResult _ msg Nothing) -> pure $ mkTextContent msg
 
     -- All other tools go through REPL
     _ -> do
@@ -958,11 +962,15 @@ handleAgdaTool stateRef tool = do
       -- Format response based on requested format (default: Concise)
       let responseFormat = Format.getFormat tool
       let responseText = Format.formatResponse responseFormat jsonValue
-      pure $ MCP.Server.ContentText responseText
+      pure $ mkTextContent responseText
+
+-- | Helper to create text resource contents
+mkTextResource :: Text -> Text -> Maybe Text -> ResourceContents
+mkTextResource resourceUri txt mimeType = TextResource $ TextResourceContents resourceUri txt mimeType Nothing
 
 -- MCP Resource Handler - exposes Agda file information as resources
 -- Resources extract parameters from the URI path
-handleAgdaResource :: IORef ServerState -> MCP.Server.URI -> AgdaMCP.Types.AgdaResource -> IO MCP.Server.ResourceContent
+handleAgdaResource :: IORef ServerState -> Text -> AgdaMCP.Types.AgdaResource -> IO ResourceContents
 handleAgdaResource stateRef uri resource = do
   result <- runTCMTop $ case resource of
     AgdaMCP.Types.Goals -> do
@@ -983,13 +991,13 @@ handleAgdaResource stateRef uri resource = do
 
   case result of
     Left err ->
-      pure $ MCP.Server.ResourceText uri "text/plain" $ "Error: " <> T.pack (show err)
+      pure $ mkTextResource uri ("Error: " <> T.pack (show err)) (Just "text/plain")
     Right agdaRes ->
       case agdaResult agdaRes of
         Nothing ->
-          pure $ MCP.Server.ResourceText uri "text/plain" $ message agdaRes
+          pure $ mkTextResource uri (message agdaRes) (Just "text/plain")
         Just val ->
-          pure $ MCP.Server.ResourceText uri "application/json" $ TE.decodeUtf8 $ LBS.toStrict $ JSON.encode val
+          pure $ mkTextResource uri (TE.decodeUtf8 $ LBS.toStrict $ JSON.encode val) (Just "application/json")
 
 -- ============================================================================
 -- Session-based Handlers (Multi-agent Support)
@@ -1020,22 +1028,22 @@ initSessionManager = do
 
 -- | Session-aware tool handler
 -- Extracts sessionId from tool, gets or creates session, routes to appropriate ServerState
-handleAgdaToolWithSession :: SessionManager.SessionManager ServerState -> AgdaMCP.Types.AgdaTool -> IO MCP.Server.Content
+handleAgdaToolWithSession :: SessionManager.SessionManager ServerState -> AgdaMCP.Types.AgdaTool -> IO Content
 handleAgdaToolWithSession manager tool = do
   -- Extract session ID from tool (all tools now have this field)
-  let sessionId = AgdaMCP.Types.sessionId tool
+  let sessionIdVal = AgdaMCP.Types.sessionId tool
 
   -- Get or create session
-  stateRef <- SessionManager.getOrCreateSession manager sessionId
+  stateRef <- SessionManager.getOrCreateSession manager sessionIdVal
 
   -- Update last used timestamp
-  SessionManager.updateLastUsed manager sessionId
+  SessionManager.updateLastUsed manager sessionIdVal
 
   -- Route to existing handler
   handleAgdaTool stateRef tool
 
 -- | Session-aware resource handler
-handleAgdaResourceWithSession :: SessionManager.SessionManager ServerState -> MCP.Server.URI -> AgdaMCP.Types.AgdaResource -> IO MCP.Server.ResourceContent
+handleAgdaResourceWithSession :: SessionManager.SessionManager ServerState -> Text -> AgdaMCP.Types.AgdaResource -> IO ResourceContents
 handleAgdaResourceWithSession manager uri resource = do
   -- Resources don't have sessionId parameter, so use default session
   -- In the future, we could extract session from URI query parameters
diff --git a/test/AgdaMCP/EditPersistenceSpec.hs b/test/AgdaMCP/EditPersistenceSpec.hs
index c577d82..1d73c1e 100644
--- a/test/AgdaMCP/EditPersistenceSpec.hs
+++ b/test/AgdaMCP/EditPersistenceSpec.hs
@@ -14,14 +14,15 @@ import qualified Data.Text.Encoding as TE
 import qualified Data.ByteString.Lazy as LBS
 import Data.Text (Text)
 import System.FilePath ((</>), takeDirectory, takeFileName)
-import System.Directory (getCurrentDirectory, copyFile, createDirectoryIfMissing, removeFile, removeDirectoryRecursive, getTemporaryDirectory)
+import System.Directory (copyFile, createDirectoryIfMissing, removeFile, removeDirectoryRecursive, getTemporaryDirectory)
 import System.Random (randomIO)
 import Control.Exception (try, SomeException, bracket, catch)
+import Paths_agda_mcp (getDataDir)
 
 import AgdaMCP.Server
 import qualified AgdaMCP.Types as Types
 import qualified AgdaMCP.SessionManager as SessionManager
-import qualified MCP.Server as MCP
+import MCP.Types (Content, ContentBlock(..), TextContent(..))
 import AgdaMCP.TestUtils (withTempTestFile)
 
 -- | Simple test case type
@@ -70,10 +71,10 @@ assertNotContains needle haystack =
 -- | Custom version for edit-persistence subdirectory
 copyEditTestFile :: FilePath -> IO FilePath
 copyEditTestFile filename = do
-  cwd <- getCurrentDirectory
+  dataDir <- getDataDir
   tmpDir <- getTemporaryDirectory
   randomHash <- randomIO :: IO Int
-  let sourceFile = cwd </> "test" </> "edit-persistence" </> filename
+  let sourceFile = dataDir </> "edit-persistence" </> filename
   let tempDir = tmpDir </> ("agda-mcp-persist-test-" ++ show (abs randomHash))
   let tempFile = tempDir </> filename
   createDirectoryIfMissing True tempDir
@@ -103,7 +104,7 @@ getGoalCount manager sessionId = do
   let tool = Types.AgdaGetGoals { Types.sessionId = Just sessionId, Types.format = Just "Full" }
   result <- handleAgdaToolWithSession manager tool
   case result of
-    MCP.ContentText txt -> do
+    TextContentType (TextContent _ txt _ _) -> do
       case JSON.decode (LBS.fromStrict $ TE.encodeUtf8 txt) of
         Just (JSON.Object obj) -> do
           case JSON.KeyMap.lookup (JSON.Key.fromText "info") obj of
diff --git a/test/AgdaMCP/MultiAgentSpec.hs b/test/AgdaMCP/MultiAgentSpec.hs
index 27a8760..2ee7936 100644
--- a/test/AgdaMCP/MultiAgentSpec.hs
+++ b/test/AgdaMCP/MultiAgentSpec.hs
@@ -25,7 +25,7 @@ import System.IO.Unsafe (unsafePerformIO)
 import AgdaMCP.Server
 import qualified AgdaMCP.Types as Types
 import qualified AgdaMCP.SessionManager as SessionManager
-import qualified MCP.Server as MCP
+import MCP.Types (Content, ContentBlock(..), TextContent(..))
 import AgdaMCP.TestUtils (withTempTestFile)
 
 -- | Simple test case type
@@ -65,11 +65,11 @@ runTool manager tool = do
   let toolWithFullFormat = setFormat tool (Just "Full")
   result <- handleAgdaToolWithSession manager toolWithFullFormat
   case result of
-    MCP.ContentText txt -> do
+    TextContentType (TextContent _ txt _ _) -> do
       case JSON.decode (LBS.fromStrict $ TE.encodeUtf8 txt) of
         Just val -> pure val
         Nothing -> fail $ "Failed to parse JSON response: " ++ T.unpack txt
-    _ -> fail "Expected ContentText response"
+    _ -> fail "Expected TextContent response"
 
 -- | Helper to run a tool and get the response as Text (forces Concise format)
 runToolConcise :: SessionManager.SessionManager ServerState -> Types.AgdaTool -> IO Text
@@ -78,8 +78,8 @@ runToolConcise manager tool = do
   let toolWithConciseFormat = setFormat tool (Just "Concise")
   result <- handleAgdaToolWithSession manager toolWithConciseFormat
   case result of
-    MCP.ContentText txt -> pure txt
-    _ -> fail "Expected ContentText response"
+    TextContentType (TextContent _ txt _ _) -> pure txt
+    _ -> fail "Expected TextContent response"
 
 -- | Set format on a tool (preserves sessionId) - simplified for GetGoals and other tools
 setFormat :: Types.AgdaTool -> Maybe Text -> Types.AgdaTool
diff --git a/test/AgdaMCP/ServerSpec.hs b/test/AgdaMCP/ServerSpec.hs
index 9339c1c..3bda55c 100644
--- a/test/AgdaMCP/ServerSpec.hs
+++ b/test/AgdaMCP/ServerSpec.hs
@@ -24,7 +24,7 @@ import System.Timeout (timeout)
 import AgdaMCP.Server
 import qualified AgdaMCP.Types as Types
 import qualified AgdaMCP.SessionManager as SessionManager
-import qualified MCP.Server as MCP
+import MCP.Types (Content, ContentBlock(..), TextContent(..))
 import qualified AgdaMCP.MultiAgentSpec as MultiAgent
 import AgdaMCP.TestUtils (withTempTestFile)
 
@@ -65,11 +65,11 @@ runTool manager tool = do
   let toolWithFullFormat = setFormat tool (Just "Full")
   result <- handleAgdaToolWithSession manager toolWithFullFormat
   case result of
-    MCP.ContentText txt -> do
+    TextContentType (TextContent _ txt _ _) -> do
       case JSON.decode (LBS.fromStrict $ TE.encodeUtf8 txt) of
         Just val -> pure val
         Nothing -> fail $ "Failed to parse JSON response: " ++ T.unpack txt
-    _ -> fail "Expected ContentText response"
+    _ -> fail "Expected TextContent response"
 
 -- | Helper to run a tool and get concise text response
 runToolConcise :: SessionManager.SessionManager ServerState -> Types.AgdaTool -> IO Text
@@ -78,8 +78,8 @@ runToolConcise manager tool = do
   let toolWithConciseFormat = setFormat tool (Just "Concise")
   result <- handleAgdaToolWithSession manager toolWithConciseFormat
   case result of
-    MCP.ContentText txt -> pure txt
-    _ -> fail "Expected ContentText response"
+    TextContentType (TextContent _ txt _ _) -> pure txt
+    _ -> fail "Expected TextContent response"
 
 -- | Set format on a tool (preserves sessionId)
 setFormat :: Types.AgdaTool -> Maybe Text -> Types.AgdaTool
@@ -973,8 +973,8 @@ goalAtPositionTests = testGroup "agda_goal_at_position"
       result <- handleAgdaToolWithSession manager tool
 
       case result of
-        MCP.ContentText txt -> assertBool "Should mention no goal found" (T.isInfixOf "No goal found" txt)
-        _ -> assertFailure "Expected ContentText response"
+        TextContentType (TextContent _ txt _ _) -> assertBool "Should mention no goal found" (T.isInfixOf "No goal found" txt)
+        _ -> assertFailure "Expected TextContent response"
 
   , withSessionManager $ \getManager ->simpleTestCase "formats concisely" $ do
       manager <- getManager
diff --git a/test/AgdaMCP/TestUtils.hs b/test/AgdaMCP/TestUtils.hs
index 60a4e76..81be961 100644
--- a/test/AgdaMCP/TestUtils.hs
+++ b/test/AgdaMCP/TestUtils.hs
@@ -8,9 +8,10 @@ module AgdaMCP.TestUtils
   ) where
 
 import System.FilePath ((</>), takeDirectory)
-import System.Directory (getCurrentDirectory, copyFile, createDirectoryIfMissing, removeDirectoryRecursive, getTemporaryDirectory)
+import System.Directory (copyFile, createDirectoryIfMissing, removeDirectoryRecursive, getTemporaryDirectory)
 import System.Random (randomIO)
 import Control.Exception (SomeException, bracket, catch)
+import Paths_agda_mcp (getDataDir)
 
 -- ============================================================================
 -- Temp File Utilities (for tests that modify files)
@@ -20,10 +21,10 @@ import Control.Exception (SomeException, bracket, catch)
 -- Uses random temp directory to preserve module name and avoid conflicts
 copyTestFile :: FilePath -> IO FilePath
 copyTestFile filename = do
-  cwd <- getCurrentDirectory
+  dataDir <- getDataDir
   tmpDir <- getTemporaryDirectory
   randomHash <- randomIO :: IO Int
-  let sourceFile = cwd </> "test" </> filename
+  let sourceFile = dataDir </> filename
   let tempDir = tmpDir </> ("agda-mcp-test-" ++ show (abs randomHash))
   let tempFile = tempDir </> filename
   createDirectoryIfMissing True tempDir