diff --git a/build.gradle.kts b/build.gradle.kts
index 8223024eeb..4d9773dec8 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -22,6 +22,7 @@ tasks.register("validateProjectList") {
             project(":usvm-python"),
             project(":usvm-ts"),
             project(":usvm-ts-dataflow"),
+            project(":usvm-mcp"),
         )
 
         // Gather the actual subprojects from the current root project.
diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index fe81c5630b..e3f6a61edb 100644
--- a/buildSrc/src/main/kotlin/Dependencies.kt
+++ b/buildSrc/src/main/kotlin/Dependencies.kt
@@ -16,6 +16,7 @@ object Versions {
     const val kotlinx_serialization = "1.7.3"
     const val ksmt = "0.5.26"
     const val logback = "1.4.8"
+    const val mcp_kotlin_sdk = "0.8.3"
     const val mockk = "1.13.4"
     const val rd = "2023.2.0"
     const val sarif4k = "0.5.0"
@@ -248,6 +249,13 @@ object Libs {
         name = "clikt",
         version = Versions.clikt
     )
+
+    // https://github.com/modelcontextprotocol/kotlin-sdk
+    val mcp_kotlin_sdk = dep(
+        group = "io.modelcontextprotocol",
+        name = "kotlin-sdk",
+        version = Versions.mcp_kotlin_sdk
+    )
 }
 
 object Plugins {
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 428d679fce..628c4a83b6 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -39,6 +39,7 @@ include("usvm-sample-language")
 include("usvm-dataflow")
 include("usvm-jvm-dataflow")
 include("usvm-ts-dataflow")
+include("usvm-mcp")
 
 include("usvm-python")
 include("usvm-python:cpythonadapter")
diff --git a/usvm-mcp/README.md b/usvm-mcp/README.md
new file mode 100644
index 0000000000..1c5dfb7ebb
--- /dev/null
+++ b/usvm-mcp/README.md
@@ -0,0 +1,163 @@
+# usvm-mcp
+
+An [MCP (Model Context Protocol)](https://modelcontextprotocol.io) server that exposes the USVM
+symbolic execution engine for TypeScript (`usvm-ts`) as a set of tools for LLM agents
+(Claude Code, Claude Desktop, MCP Inspector, or any other MCP client).
+
+The goal is **hybrid analysis of dynamic languages**: the LLM reads and writes code,
+while the symbolic machine provides ground-truth facts about it — concrete inputs per
+execution path, reachability witnesses, crashing inputs, and counterexamples to
+hypotheses formulated by the LLM.
+
+## Prerequisites
+
+1. **JDK 11+** — the MCP Kotlin SDK requires JVM 11 (the rest of USVM targets 1.8;
+   this leaf module overrides the target).
+2. **Node.js** — used by ArkAnalyzer to convert TypeScript into ETS IR.
+3. **ArkAnalyzer** — a built checkout, pointed to by the `ARKANALYZER_DIR` environment variable:
+
+   ```bash
+   git clone https://gitee.com/openharmony-sig/arkanalyzer
+   cd arkanalyzer && npm install && npm run build
+   export ARKANALYZER_DIR=$(pwd)
+   ```
+
+## Build and run
+
+```bash
+./gradlew :usvm-mcp:installDist
+```
+
+This produces a launcher at `usvm-mcp/build/install/usvm-mcp/bin/usvm-mcp`.
+The server speaks MCP over **stdio**: stdout carries JSON-RPC, all logging goes to stderr.
+
+### Connect from Claude Code
+
+```bash
+claude mcp add usvm \
+  -e ARKANALYZER_DIR=/path/to/arkanalyzer \
+  -- /path/to/usvm/usvm-mcp/build/install/usvm-mcp/bin/usvm-mcp
+```
+
+### Connect from MCP Inspector (debugging)
+
+```bash
+ARKANALYZER_DIR=/path/to/arkanalyzer \
+  npx @modelcontextprotocol/inspector usvm-mcp/build/install/usvm-mcp/bin/usvm-mcp
+```
+
+### Run from Gradle (debugging)
+
+```bash
+./gradlew :usvm-mcp:run
+```
+
+## Tools
+
+All tools take a `file` argument — a path to a single `.ts` file. Converted scenes are
+cached in memory (keyed by path and mtime), so repeated calls on the same file are fast.
+Analysis tools also accept `timeoutMs` (default 30000, max 300000).
+
+| Tool | What it does |
+|------|--------------|
+| `list_methods` | Lists classes and methods visible to the machine. Call it first to discover exact `class`/`method` argument values. Top-level functions live in a synthetic `%dflt` class. |
+| `get_method_ir` | Dumps the CFG of a method: IR statements with indices and successor indices. **Statement indices are the only way to address a statement** (source line numbers are not preserved in the IR); pass them as `stmtIndex` to `check_reachability`. |
+| `generate_tests` | Symbolically executes a method and returns one test case per explored path: concrete `parameters`/`thisInstance` plus the expected return value or exception. |
+| `check_exceptions` | Same exploration, but reports only the paths that throw, together with the inputs that trigger them. |
+| `check_reachability` | Directed (targeted) search towards a given statement. Returns `REACHABLE` with a witness (concrete inputs) or `NOT_REACHED_WITHIN_BUDGET`. |
+| `find_unreachable_code` | Reports `if` branches never taken during exploration — dead-code candidates (statement indices match `get_method_ir`). |
+| `find_counterexample` | Tries to **falsify a boolean property function** written by the LLM: searches for inputs where it returns `false` (counterexamples) or throws (crashes). |
+
+### Result format
+
+Analysis results are JSON. Concrete values map to JSON naturally; JS-specific values are
+tagged objects so nothing is ambiguous:
+
+```json
+{
+  "kind": "SUCCESS",
+  "thisInstance": { "$kind": "object", "class": "BasicConditions", "properties": {} },
+  "parameters": [ 12.0, { "$kind": "number", "value": "NaN" }, { "$kind": "undefined" } ],
+  "returnValue": 1.0
+}
+```
+
+Exceptional paths use `"kind": "EXCEPTION"` with an `exception` object instead of `returnValue`.
+
+## Hybrid workflows
+
+**Test generation.** `generate_tests` yields per-path inputs and outcomes; the LLM turns
+them into a unit-test file with real assertions and can immediately execute it to validate.
+
+**Reachability querying.** `get_method_ir` → pick the index of an interesting statement
+(a `return`, a branch) → `check_reachability`. A witness is a ready-made regression input.
+
+**Hypothesis falsification** (`find_counterexample`). The LLM writes a property function
+into a `.ts` file and asks the machine to break it:
+
+```typescript
+function abs(x: number): number {
+    if (x < 0) return -x;
+    return x;
+}
+
+// Hypothesis: "abs is always non-negative"
+function propAbsNonNegative(x: number): boolean {
+    return abs(x) >= 0;
+}
+```
+
+`find_counterexample(file, method="propAbsNonNegative")` → `COUNTEREXAMPLE_FOUND` with
+concrete falsifying inputs, or `NO_COUNTEREXAMPLE_WITHIN_BUDGET`.
+
+**Equivalence checking of a refactoring.** A special case of the above: the LLM puts the
+original `f`, its refactored `g`, and `function equiv(x: number): boolean { return f(x) === g(x); }`
+into one file and falsifies `equiv`. A counterexample is an input where the refactoring
+changed behavior.
+
+## Interpreting verdicts honestly
+
+- Exploration is **bounded by a time budget**. `NOT_REACHED_WITHIN_BUDGET`,
+  an empty `check_exceptions` result, or `NO_COUNTEREXAMPLE_WITHIN_BUDGET` are
+  *evidence*, not proofs. Retry with a larger `timeoutMs` when it matters.
+- The symbolic model **over-approximates JavaScript semantics** in places
+  (e.g., number comparisons involving `NaN` and untyped values), so a `REACHABLE`
+  witness may occasionally be spurious. The recommended hybrid loop is to
+  **validate every witness by actually running the code** with the reported inputs
+  (node/ts-node) — the tool responses remind about this. The same over-approximation
+  can make `find_unreachable_code` miss dead branches.
+- The property/code for `find_counterexample` must live in a **single `.ts` file**
+  (project-level scenes are not wired up yet), and must stay within the TS subset
+  supported by `usvm-ts` (numbers, booleans, objects, arrays; strings partially).
+
+## Module layout
+
+```
+src/main/kotlin/org/usvm/mcp/
+├── Main.kt                  # stdio transport, stdout guard
+├── UsvmMcpServer.kt         # server construction, tool registration
+├── McpErrors.kt             # expected-failure handling (isError results)
+├── scene/                   # EtsScene cache (ArkAnalyzer), method lookup
+├── exec/                    # UMachineOptions presets, serialized machine runs
+├── json/                    # DTOs and TsTestValue -> JSON rendering
+└── tools/                   # one file per MCP tool
+```
+
+Design notes:
+
+- **stdout discipline**: stdout is the JSON-RPC channel. `Main.kt` re-points `System.out`
+  to stderr before anything else, and `logback.xml` sends all logging to stderr
+  (`org.usvm`/`org.jacodb`/`io.ksmt` are capped at `WARN`).
+- **One analysis at a time**: machine runs are serialized with a mutex; MCP clients may
+  issue concurrent calls, but the solver and the machine are heavyweight.
+- Concrete values are resolved from symbolic states by `TsTestResolver`
+  (`usvm-ts`, `org.usvm.util`), shared with the usvm-ts test infrastructure.
+
+## Tests
+
+```bash
+./gradlew :usvm-mcp:test       # unit tests (no ArkAnalyzer required)
+```
+
+For an end-to-end check, use the MCP Inspector recipe above on
+`usvm-ts/src/test/resources/reachability/BasicConditions.ts`.
diff --git a/usvm-mcp/build.gradle.kts b/usvm-mcp/build.gradle.kts
new file mode 100644
index 0000000000..ff9e8d0133
--- /dev/null
+++ b/usvm-mcp/build.gradle.kts
@@ -0,0 +1,48 @@
+import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
+
+plugins {
+    id("usvm.kotlin-conventions")
+    kotlin("plugin.serialization") version Versions.kotlin
+    application
+    id(Plugins.Shadow)
+}
+
+dependencies {
+    implementation(project(":usvm-ts"))
+    implementation(project(":usvm-core"))
+    implementation(project(":usvm-util"))
+
+    implementation(Libs.jacodb_ets)
+    implementation(Libs.mcp_kotlin_sdk)
+    implementation(Libs.kotlinx_serialization_json)
+
+    runtimeOnly(Libs.logback)
+}
+
+// The MCP Kotlin SDK (and its Ktor/kotlinx-io dependencies) requires JVM 11,
+// while the shared conventions target JVM 1.8. This is a leaf application
+// module, so it is safe to raise the target here.
+tasks.withType<JavaCompile> {
+    sourceCompatibility = JavaVersion.VERSION_11.toString()
+    targetCompatibility = JavaVersion.VERSION_11.toString()
+}
+tasks.withType<KotlinCompile> {
+    kotlinOptions {
+        jvmTarget = JavaVersion.VERSION_11.toString()
+    }
+}
+
+application {
+    mainClass = "org.usvm.mcp.MainKt"
+    applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8")
+}
+
+tasks.startScripts {
+    applicationName = "usvm-mcp"
+}
+
+// Forward stdin to the process so that `./gradlew :usvm-mcp:run` can be used
+// as an MCP stdio server directly (e.g., for local debugging).
+tasks.named<JavaExec>("run") {
+    standardInput = System.`in`
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/Main.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/Main.kt
new file mode 100644
index 0000000000..54a6036925
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/Main.kt
@@ -0,0 +1,36 @@
+package org.usvm.mcp
+
+import io.modelcontextprotocol.kotlin.sdk.server.StdioServerTransport
+import kotlinx.coroutines.CompletableDeferred
+import kotlinx.coroutines.runBlocking
+import kotlinx.io.asSink
+import kotlinx.io.asSource
+import kotlinx.io.buffered
+import java.io.FileDescriptor
+import java.io.FileOutputStream
+import java.io.PrintStream
+
+/**
+ * Entry point of the USVM MCP server (stdio transport).
+ *
+ * Stdout is the JSON-RPC channel, so before anything else we redirect
+ * [System.out] to stderr: any stray `println` from USVM/ksmt/ArkAnalyzer
+ * integration must not corrupt the protocol stream.
+ */
+fun main() {
+    val realStdout = System.out
+    System.setOut(PrintStream(FileOutputStream(FileDescriptor.err), true))
+
+    val server = buildUsvmMcpServer()
+    val transport = StdioServerTransport(
+        System.`in`.asSource().buffered(),
+        realStdout.asSink().buffered(),
+    )
+
+    runBlocking {
+        val session = server.createSession(transport)
+        val done = CompletableDeferred<Unit>()
+        session.onClose { done.complete(Unit) }
+        done.await()
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/McpErrors.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/McpErrors.kt
new file mode 100644
index 0000000000..233fdc84ad
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/McpErrors.kt
@@ -0,0 +1,32 @@
+package org.usvm.mcp
+
+import io.modelcontextprotocol.kotlin.sdk.types.CallToolResult
+import io.modelcontextprotocol.kotlin.sdk.types.TextContent
+
+/**
+ * An expected, user-facing tool failure. Its message is written as an
+ * actionable instruction for the calling LLM/user (what went wrong and
+ * how to fix the call or the environment).
+ */
+class McpToolException(message: String) : RuntimeException(message)
+
+fun textResult(text: String): CallToolResult =
+    CallToolResult(content = listOf(TextContent(text)))
+
+fun errorResult(text: String): CallToolResult =
+    CallToolResult(content = listOf(TextContent(text)), isError = true)
+
+/**
+ * Wraps a tool handler body: expected errors become `isError` results with
+ * actionable messages, unexpected ones become `isError` results with a short
+ * diagnostic. The server never crashes because of a single tool call.
+ */
+suspend fun runTool(block: suspend () -> CallToolResult): CallToolResult =
+    try {
+        block()
+    } catch (e: McpToolException) {
+        errorResult(e.message ?: "Tool failed")
+    } catch (@Suppress("TooGenericExceptionCaught") e: Throwable) {
+        val frames = e.stackTrace.take(5).joinToString("\n") { "  at $it" }
+        errorResult("Internal error: ${e::class.simpleName}: ${e.message}\n$frames")
+    }
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/UsvmMcpServer.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/UsvmMcpServer.kt
new file mode 100644
index 0000000000..9848fd4915
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/UsvmMcpServer.kt
@@ -0,0 +1,58 @@
+package org.usvm.mcp
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import io.modelcontextprotocol.kotlin.sdk.server.ServerOptions
+import io.modelcontextprotocol.kotlin.sdk.types.Implementation
+import io.modelcontextprotocol.kotlin.sdk.types.ServerCapabilities
+import org.usvm.mcp.exec.TsAnalysisRunner
+import org.usvm.mcp.scene.SceneCache
+import org.usvm.mcp.tools.UsvmToolContext
+import org.usvm.mcp.tools.registerCheckExceptionsTool
+import org.usvm.mcp.tools.registerCheckReachabilityTool
+import org.usvm.mcp.tools.registerFindCounterexampleTool
+import org.usvm.mcp.tools.registerFindUnreachableCodeTool
+import org.usvm.mcp.tools.registerGenerateTestsTool
+import org.usvm.mcp.tools.registerGetMethodIrTool
+import org.usvm.mcp.tools.registerListMethodsTool
+
+const val SERVER_NAME = "usvm-mcp"
+const val SERVER_VERSION = "0.1.0"
+
+private const val SERVER_INSTRUCTIONS = """
+USVM symbolic execution tools for TypeScript.
+
+Typical hybrid workflow:
+1. `list_methods` to see what is analyzable in a .ts file;
+2. `get_method_ir` to inspect the CFG of a method (statement indices are used as targets);
+3. `generate_tests` / `check_exceptions` to obtain concrete inputs per execution path;
+4. `check_reachability` with a statement index from `get_method_ir`;
+5. `find_unreachable_code` for dead branches;
+6. `find_counterexample` to falsify a boolean property function you wrote yourself.
+
+Analysis budgets are limited: a negative answer means "not found within budget",
+not a proof, unless stated otherwise.
+"""
+
+/**
+ * Builds the MCP server and registers all USVM tools on it.
+ */
+fun buildUsvmMcpServer(): Server {
+    val server = Server(
+        serverInfo = Implementation(name = SERVER_NAME, version = SERVER_VERSION),
+        options = ServerOptions(
+            capabilities = ServerCapabilities(tools = ServerCapabilities.Tools(listChanged = false)),
+        ),
+        instructions = SERVER_INSTRUCTIONS.trimIndent(),
+    )
+
+    val ctx = UsvmToolContext(scenes = SceneCache(), runner = TsAnalysisRunner())
+    server.registerListMethodsTool(ctx)
+    server.registerGetMethodIrTool(ctx)
+    server.registerGenerateTestsTool(ctx)
+    server.registerCheckExceptionsTool(ctx)
+    server.registerCheckReachabilityTool(ctx)
+    server.registerFindUnreachableCodeTool(ctx)
+    server.registerFindCounterexampleTool(ctx)
+
+    return server
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/AnalysisOptions.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/AnalysisOptions.kt
new file mode 100644
index 0000000000..679271ec24
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/AnalysisOptions.kt
@@ -0,0 +1,42 @@
+package org.usvm.mcp.exec
+
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.UMachineOptions
+import kotlin.time.Duration
+import kotlin.time.Duration.Companion.seconds
+
+/**
+ * Factories for [UMachineOptions] used by the MCP tools. Mirrors the option
+ * sets battle-tested in usvm-ts test infrastructure (`TsMethodTestRunner`,
+ * reachability tests), but with finite, caller-controlled budgets.
+ */
+object AnalysisOptions {
+
+    /** Path exploration aimed at covering new code: test generation, exceptions. */
+    fun coverage(timeout: Duration): UMachineOptions = UMachineOptions(
+        pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
+        exceptionsPropagation = true,
+        timeout = timeout,
+        stepsFromLastCovered = STEPS_FROM_LAST_COVERED,
+        solverType = SolverType.YICES,
+        solverTimeout = SOLVER_TIMEOUT,
+        typeOperationsTimeout = TYPE_OPERATIONS_TIMEOUT,
+    )
+
+    /** Directed exploration towards a reachability target. */
+    fun targeted(timeout: Duration): UMachineOptions = UMachineOptions(
+        pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
+        exceptionsPropagation = true,
+        stopOnTargetsReached = true,
+        timeout = timeout,
+        stepsFromLastCovered = STEPS_FROM_LAST_COVERED,
+        solverType = SolverType.YICES,
+        solverTimeout = SOLVER_TIMEOUT,
+        typeOperationsTimeout = TYPE_OPERATIONS_TIMEOUT,
+    )
+
+    private const val STEPS_FROM_LAST_COVERED = 3500L
+    private val SOLVER_TIMEOUT = 5.seconds
+    private val TYPE_OPERATIONS_TIMEOUT = 1.seconds
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/TsAnalysisRunner.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/TsAnalysisRunner.kt
new file mode 100644
index 0000000000..2e562870c0
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/TsAnalysisRunner.kt
@@ -0,0 +1,106 @@
+package org.usvm.mcp.exec
+
+import kotlinx.coroutines.Dispatchers
+import kotlinx.coroutines.runInterruptible
+import kotlinx.coroutines.sync.Mutex
+import kotlinx.coroutines.sync.withLock
+import mu.KotlinLogging
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsStmt
+import org.usvm.api.TsTest
+import org.usvm.api.checkers.UncoveredIfSuccessors
+import org.usvm.api.checkers.UnreachableCodeDetector
+import org.usvm.api.targets.ReachabilityObserver
+import org.usvm.api.targets.TsReachabilityTarget
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.machine.state.TsState
+import org.usvm.util.TsTestResolver
+import kotlin.time.Duration
+
+private val logger = KotlinLogging.logger {}
+
+/** A symbolic state either resolved to a concrete test or failed to resolve. */
+data class ResolvedCase(
+    val test: TsTest?,
+    val error: String?,
+)
+
+data class ReachabilityOutcome(
+    val reached: Boolean,
+    val witness: ResolvedCase?,
+)
+
+/**
+ * Runs USVM analyses over TypeScript methods.
+ *
+ * All runs are serialized through a [Mutex]: the machine and the SMT solver
+ * are heavyweight, and MCP clients may issue concurrent calls.
+ */
+class TsAnalysisRunner {
+
+    private val mutex = Mutex()
+
+    /** Explores the method and resolves every collected state to concrete inputs/outcome. */
+    suspend fun runTests(scene: EtsScene, method: EtsMethod, timeout: Duration): List<ResolvedCase> =
+        withMachineLock {
+            val options = AnalysisOptions.coverage(timeout)
+            TsMachine(scene, options, TsOptions()).use { machine ->
+                val states = machine.analyze(listOf(method))
+                states.map { resolveState(method, it) }
+            }
+        }
+
+    /** Directed search for a path reaching [target] inside [method]. */
+    suspend fun runReachability(
+        scene: EtsScene,
+        method: EtsMethod,
+        target: EtsStmt,
+        timeout: Duration,
+    ): ReachabilityOutcome = withMachineLock {
+        val options = AnalysisOptions.targeted(timeout)
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        initialTarget.addChild(TsReachabilityTarget.FinalPoint(target))
+
+        TsMachine(scene, options, TsOptions(), machineObserver = ReachabilityObserver()).use { machine ->
+            val states = machine.analyze(listOf(method), listOf(initialTarget))
+            val witnessState = states.firstOrNull { target in it.pathNode.allStatements }
+            ReachabilityOutcome(
+                reached = witnessState != null,
+                witness = witnessState?.let { resolveState(method, it) },
+            )
+        }
+    }
+
+    /** Searches for `if` branches never taken during exploration of [methods]. */
+    suspend fun runUnreachableDetection(
+        scene: EtsScene,
+        methods: List<EtsMethod>,
+        timeout: Duration,
+    ): Map<EtsMethod, List<UncoveredIfSuccessors>> = withMachineLock {
+        val options = AnalysisOptions.coverage(timeout)
+        val detector = UnreachableCodeDetector()
+        // The detector observes both the machine and the interpreter, so it is passed twice.
+        val tsOptions = TsOptions(interproceduralAnalysis = false)
+        TsMachine(scene, options, tsOptions, detector, detector).use { machine ->
+            machine.analyze(methods)
+        }
+        detector.result
+    }
+
+    private fun resolveState(method: EtsMethod, state: TsState): ResolvedCase =
+        try {
+            ResolvedCase(test = TsTestResolver().resolve(method, state), error = null)
+        } catch (@Suppress("TooGenericExceptionCaught") e: Throwable) {
+            logger.warn(e) { "Failed to resolve a symbolic state of ${method.name}" }
+            ResolvedCase(test = null, error = "${e::class.simpleName}: ${e.message}")
+        }
+
+    private suspend fun <T> withMachineLock(block: () -> T): T =
+        mutex.withLock {
+            runInterruptible(Dispatchers.IO) {
+                block()
+            }
+        }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/json/Dtos.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/json/Dtos.kt
new file mode 100644
index 0000000000..36c483281a
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/json/Dtos.kt
@@ -0,0 +1,129 @@
+package org.usvm.mcp.json
+
+import kotlinx.serialization.Serializable
+import kotlinx.serialization.json.Json
+import kotlinx.serialization.json.JsonElement
+
+/** JSON configuration shared by all tool responses. */
+val McpJson: Json = Json {
+    prettyPrint = true
+    encodeDefaults = true
+    explicitNulls = false
+}
+
+@Serializable
+data class ExceptionDto(
+    val type: String,
+    val message: String? = null,
+    val value: JsonElement? = null,
+)
+
+/**
+ * One symbolic execution path rendered as a concrete test case:
+ * concrete inputs plus the observed outcome.
+ */
+@Serializable
+data class TestCaseDto(
+    val kind: String, // SUCCESS | EXCEPTION | UNRESOLVED
+    val thisInstance: JsonElement? = null,
+    val parameters: List<JsonElement> = emptyList(),
+    val returnValue: JsonElement? = null,
+    val exception: ExceptionDto? = null,
+    val resolutionError: String? = null,
+)
+
+@Serializable
+data class GenerateTestsResultDto(
+    val method: String,
+    val testCases: List<TestCaseDto>,
+    val note: String,
+)
+
+@Serializable
+data class CheckExceptionsResultDto(
+    val method: String,
+    val exceptionalCases: List<TestCaseDto>,
+    val totalPathsExplored: Int,
+    val note: String,
+)
+
+@Serializable
+data class ReachabilityResultDto(
+    val method: String,
+    val stmtIndex: Int,
+    val statement: String,
+    val status: String, // REACHABLE | NOT_REACHED_WITHIN_BUDGET
+    val witness: TestCaseDto? = null,
+    val note: String,
+)
+
+@Serializable
+data class StmtRefDto(
+    val index: Int,
+    val text: String,
+)
+
+@Serializable
+data class UnreachableFindingDto(
+    val method: String,
+    val ifStmtIndex: Int,
+    val ifStmt: String,
+    val uncoveredSuccessors: List<StmtRefDto>,
+)
+
+@Serializable
+data class UnreachableCodeResultDto(
+    val findings: List<UnreachableFindingDto>,
+    val analyzedMethods: List<String>,
+    val note: String,
+)
+
+@Serializable
+data class ParamDto(
+    val name: String,
+    val type: String,
+)
+
+@Serializable
+data class MethodDto(
+    val name: String,
+    val parameters: List<ParamDto>,
+    val returnType: String,
+    val stmtCount: Int,
+)
+
+@Serializable
+data class ClassDto(
+    val name: String,
+    val methods: List<MethodDto>,
+)
+
+@Serializable
+data class ListMethodsResultDto(
+    val file: String,
+    val classes: List<ClassDto>,
+)
+
+@Serializable
+data class StmtDto(
+    val index: Int,
+    val kind: String,
+    val text: String,
+    val successors: List<Int>,
+)
+
+@Serializable
+data class MethodIrResultDto(
+    val method: String,
+    val statements: List<StmtDto>,
+)
+
+@Serializable
+data class CounterexampleResultDto(
+    val method: String,
+    val verdict: String, // COUNTEREXAMPLE_FOUND | NO_COUNTEREXAMPLE_WITHIN_BUDGET
+    val counterexamples: List<TestCaseDto>,
+    val crashes: List<TestCaseDto>,
+    val totalPathsExplored: Int,
+    val note: String,
+)
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/json/TsTestValueJson.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/json/TsTestValueJson.kt
new file mode 100644
index 0000000000..510fc22da0
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/json/TsTestValueJson.kt
@@ -0,0 +1,94 @@
+package org.usvm.mcp.json
+
+import kotlinx.serialization.json.JsonElement
+import kotlinx.serialization.json.JsonNull
+import kotlinx.serialization.json.JsonPrimitive
+import kotlinx.serialization.json.buildJsonArray
+import kotlinx.serialization.json.buildJsonObject
+import kotlinx.serialization.json.put
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+
+/**
+ * Converts [TsTestValue] trees (produced by `TsTestResolver`) into JSON
+ * suitable for an LLM: primitives map to JSON primitives, special JS values
+ * are tagged objects, so nothing is ambiguous.
+ */
+fun TsTestValue.toJson(): JsonElement = when (this) {
+    is TsTestValue.TsNull -> JsonNull
+    is TsTestValue.TsUndefined -> tagged("undefined")
+    is TsTestValue.TsAny -> tagged("any")
+    is TsTestValue.TsUnknown -> tagged("unknown")
+    is TsTestValue.TsBoolean -> JsonPrimitive(value)
+    is TsTestValue.TsString -> JsonPrimitive(value)
+    is TsTestValue.TsBigInt -> buildJsonObject {
+        put(KIND, "bigint")
+        put("value", value)
+    }
+
+    is TsTestValue.TsNumber.TsInteger -> JsonPrimitive(value)
+    is TsTestValue.TsNumber.TsDouble -> doubleToJson(value)
+
+    is TsTestValue.TsClass -> buildJsonObject {
+        put(KIND, "object")
+        put("class", name)
+        put(
+            "properties",
+            buildJsonObject {
+                properties.forEach { (key, propValue) -> put(key, propValue.toJson()) }
+            },
+        )
+    }
+
+    is TsTestValue.TsArray<*> -> buildJsonArray {
+        values.forEach { add(it.toJson()) }
+    }
+
+    is TsTestValue.TsException -> toExceptionDto().let { dto ->
+        buildJsonObject {
+            put(KIND, "exception")
+            put("type", dto.type)
+            dto.message?.let { put("message", it) }
+            dto.value?.let { put("value", it) }
+        }
+    }
+}
+
+fun TsTestValue.TsException.toExceptionDto(): ExceptionDto = when (this) {
+    is TsTestValue.TsException.StringException -> ExceptionDto(type = "string", message = message)
+    is TsTestValue.TsException.ObjectException -> ExceptionDto(type = "object", value = value.toJson())
+    is TsTestValue.TsException.UnknownException -> ExceptionDto(type = "unknown")
+}
+
+/** Renders a resolved symbolic state as a test case DTO. */
+fun TsTest.toTestCaseDto(): TestCaseDto {
+    val result = returnValue
+    return TestCaseDto(
+        kind = if (result is TsTestValue.TsException) "EXCEPTION" else "SUCCESS",
+        thisInstance = before.thisInstance?.toJson(),
+        parameters = before.parameters.map { it.toJson() },
+        returnValue = if (result is TsTestValue.TsException) null else result.toJson(),
+        exception = (result as? TsTestValue.TsException)?.toExceptionDto(),
+    )
+}
+
+fun unresolvedTestCase(error: String): TestCaseDto =
+    TestCaseDto(kind = "UNRESOLVED", resolutionError = error)
+
+private const val KIND = "\$kind"
+
+private fun tagged(kind: String): JsonElement = buildJsonObject { put(KIND, kind) }
+
+/**
+ * JS numbers include NaN and Infinities, which are not representable in JSON.
+ * They are encoded as tagged objects so the client can tell them apart from strings.
+ */
+private fun doubleToJson(value: Double): JsonElement =
+    if (value.isFinite()) {
+        JsonPrimitive(value)
+    } else {
+        buildJsonObject {
+            put(KIND, "number")
+            put("value", value.toString()) // "NaN", "Infinity", "-Infinity"
+        }
+    }
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/MethodLookup.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/MethodLookup.kt
new file mode 100644
index 0000000000..cb8dcea29c
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/MethodLookup.kt
@@ -0,0 +1,74 @@
+package org.usvm.mcp.scene
+
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsScene
+import org.usvm.mcp.McpToolException
+
+/**
+ * Locating classes and methods inside an [EtsScene] with LLM-friendly errors:
+ * every failure lists the actually available candidates.
+ */
+object MethodLookup {
+
+    /** Returns project classes, optionally filtered by [className]. */
+    fun findClasses(scene: EtsScene, className: String?): List<EtsClass> {
+        if (className == null) return scene.projectClasses
+        val matched = scene.projectClasses.filter { it.name == className }
+        if (matched.isEmpty()) {
+            val available = scene.projectClasses.joinToString(", ") { "'${it.name}'" }
+            throw McpToolException(
+                "Class '$className' is not found in the scene. Available classes: $available. " +
+                    "Note: top-level functions live in a synthetic default class; " +
+                    "omit the 'class' argument to search everywhere."
+            )
+        }
+        return matched
+    }
+
+    /**
+     * Finds a single analyzable method (a method with a non-empty CFG).
+     */
+    fun findMethod(scene: EtsScene, className: String?, methodName: String): EtsMethod {
+        val classes = findClasses(scene, className)
+        val candidates = classes
+            .flatMap { it.methods }
+            .filter { it.name == methodName }
+
+        val analyzable = candidates.filter { it.isAnalyzable() }
+
+        return when {
+            analyzable.size == 1 -> analyzable.single()
+
+            analyzable.isEmpty() && candidates.isNotEmpty() -> throw McpToolException(
+                "Method '$methodName' exists but has no body (empty CFG), so it cannot be analyzed."
+            )
+
+            analyzable.isEmpty() -> {
+                val available = classes
+                    .flatMap { cls -> cls.methods.filter { it.isAnalyzable() } }
+                    .joinToString(", ") { "'${it.enclosingClass?.name}.${it.name}'" }
+                throw McpToolException(
+                    "Method '$methodName' is not found. Available analyzable methods: $available. " +
+                        "Use the list_methods tool to inspect the file."
+                )
+            }
+
+            else -> {
+                val options = analyzable.joinToString(", ") { "'${it.enclosingClass?.name}.${it.name}'" }
+                throw McpToolException(
+                    "Method name '$methodName' is ambiguous: $options. " +
+                        "Disambiguate with the 'class' argument."
+                )
+            }
+        }
+    }
+
+    fun EtsMethod.isAnalyzable(): Boolean =
+        runCatching { cfg.stmts.isNotEmpty() }.getOrDefault(false)
+
+    fun EtsMethod.qualifiedName(): String {
+        val cls = enclosingClass?.name
+        return if (cls.isNullOrBlank()) name else "$cls.$name"
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/SceneCache.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/SceneCache.kt
new file mode 100644
index 0000000000..1bbd9f48be
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/SceneCache.kt
@@ -0,0 +1,98 @@
+package org.usvm.mcp.scene
+
+import mu.KotlinLogging
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.usvm.mcp.McpToolException
+import java.nio.file.Files
+import java.nio.file.Path
+import java.nio.file.Paths
+import java.nio.file.attribute.FileTime
+import java.util.concurrent.ConcurrentHashMap
+
+private val logger = KotlinLogging.logger {}
+
+/**
+ * Loads and caches [EtsScene]s built from single `.ts` files.
+ *
+ * Conversion `.ts -> ETS IR` is delegated to ArkAnalyzer (an external
+ * node.js tool, see [loadEtsFileAutoConvert]) and is expensive, so scenes
+ * are cached in memory, keyed by the real path and invalidated by mtime.
+ */
+class SceneCache {
+
+    private data class Entry(val mtime: FileTime, val scene: EtsScene)
+
+    private val cache = ConcurrentHashMap<Path, Entry>()
+
+    fun getScene(file: String): EtsScene {
+        val path = resolveTsFile(file)
+        val mtime = Files.getLastModifiedTime(path)
+        val cached = cache[path]
+        if (cached != null && cached.mtime == mtime) {
+            return cached.scene
+        }
+        checkArkAnalyzerAvailable()
+        logger.info { "Converting $path to ETS IR via ArkAnalyzer..." }
+        val etsFile = try {
+            // Type inference gives the machine precise `number`/`boolean` types,
+            // significantly reducing spurious paths caused by untyped values.
+            loadEtsFileAutoConvert(path, useArkAnalyzerTypeInference = 1)
+        } catch (@Suppress("TooGenericExceptionCaught") e: Throwable) {
+            throw McpToolException(
+                "Failed to convert '$path' to ETS IR via ArkAnalyzer: ${e.message}. " +
+                    "Check that the file is valid TypeScript and that ArkAnalyzer is built " +
+                    "(ARKANALYZER_DIR must point to a checkout with 'npm install && npm run build' done)."
+            )
+        }
+        val scene = EtsScene(listOf(etsFile))
+        cache[path] = Entry(mtime, scene)
+        return scene
+    }
+
+    private fun resolveTsFile(file: String): Path {
+        val path = try {
+            Paths.get(file).toRealPath()
+        } catch (@Suppress("SwallowedException") e: java.io.IOException) {
+            throw McpToolException(
+                "File not found: '$file'. Provide an absolute path (or a path relative " +
+                    "to the server working directory) to an existing .ts file."
+            )
+        }
+        if (!Files.isRegularFile(path)) {
+            throw McpToolException("'$path' is not a regular file. Provide a path to a .ts file.")
+        }
+        if (!path.fileName.toString().endsWith(".ts")) {
+            throw McpToolException(
+                "'$path' does not look like a TypeScript file (expected a '.ts' extension). " +
+                    "This server analyzes TypeScript sources only."
+            )
+        }
+        return path
+    }
+
+    private fun checkArkAnalyzerAvailable() {
+        val dirValue = System.getenv(ARKANALYZER_DIR_ENV)
+            ?: throw McpToolException(
+                "Environment variable $ARKANALYZER_DIR_ENV is not set. It must point to a checkout of " +
+                    "ArkAnalyzer (https://gitee.com/openharmony-sig/arkanalyzer) built with " +
+                    "'npm install && npm run build'. Restart the MCP server with this variable set."
+            )
+        val dir = Paths.get(dirValue)
+        if (!Files.isDirectory(dir)) {
+            throw McpToolException("$ARKANALYZER_DIR_ENV points to '$dirValue', which is not a directory.")
+        }
+        val script = dir.resolve(SERIALIZE_SCRIPT)
+        if (!Files.isRegularFile(script)) {
+            throw McpToolException(
+                "ArkAnalyzer build artifact not found: '$script'. " +
+                    "Run 'npm install && npm run build' in '$dirValue'."
+            )
+        }
+    }
+
+    companion object {
+        private const val ARKANALYZER_DIR_ENV = "ARKANALYZER_DIR"
+        private const val SERIALIZE_SCRIPT = "out/src/save/serializeArkIR.js"
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckExceptionsTool.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckExceptionsTool.kt
new file mode 100644
index 0000000000..c55be9ae70
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckExceptionsTool.kt
@@ -0,0 +1,51 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import kotlinx.serialization.encodeToString
+import org.usvm.api.TsTestValue
+import org.usvm.mcp.json.CheckExceptionsResultDto
+import org.usvm.mcp.json.McpJson
+import org.usvm.mcp.json.toTestCaseDto
+import org.usvm.mcp.runTool
+import org.usvm.mcp.scene.MethodLookup
+import org.usvm.mcp.scene.MethodLookup.qualifiedName
+import org.usvm.mcp.textResult
+
+fun Server.registerCheckExceptionsTool(ctx: UsvmToolContext) {
+    addTool(
+        name = "check_exceptions",
+        description = """
+            Searches for concrete inputs that make a TypeScript method throw an exception
+            (crash). Runs the same path exploration as generate_tests but reports only the
+            failing paths, together with the input values that trigger them. An empty result
+            means no crashing path was found within the budget. $BUDGET_NOTE
+        """.trimIndent(),
+        inputSchema = toolSchema(required = listOf("file", "method")) {
+            fileProp()
+            classProp()
+            methodProp()
+            timeoutProp()
+        },
+    ) { request ->
+        runTool {
+            val args = request.arguments
+            val scene = ctx.scenes.getScene(args.requireStringArg("file"))
+            val method = MethodLookup.findMethod(scene, args.stringArg("class"), args.requireStringArg("method"))
+            val cases = ctx.runner.runTests(scene, method, args.timeoutArg())
+            val exceptional = cases
+                .mapNotNull { it.test }
+                .filter { it.returnValue is TsTestValue.TsException }
+                .map { it.toTestCaseDto() }
+            textResult(
+                McpJson.encodeToString(
+                    CheckExceptionsResultDto(
+                        method = method.qualifiedName(),
+                        exceptionalCases = exceptional,
+                        totalPathsExplored = cases.size,
+                        note = BUDGET_NOTE,
+                    )
+                )
+            )
+        }
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckReachabilityTool.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckReachabilityTool.kt
new file mode 100644
index 0000000000..86007c4263
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckReachabilityTool.kt
@@ -0,0 +1,74 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import kotlinx.serialization.encodeToString
+import org.usvm.mcp.McpToolException
+import org.usvm.mcp.json.McpJson
+import org.usvm.mcp.json.ReachabilityResultDto
+import org.usvm.mcp.json.toTestCaseDto
+import org.usvm.mcp.json.unresolvedTestCase
+import org.usvm.mcp.runTool
+import org.usvm.mcp.scene.MethodLookup
+import org.usvm.mcp.scene.MethodLookup.qualifiedName
+import org.usvm.mcp.textResult
+
+fun Server.registerCheckReachabilityTool(ctx: UsvmToolContext) {
+    addTool(
+        name = "check_reachability",
+        description = """
+            Checks whether a specific IR statement of a TypeScript method is reachable and,
+            if so, returns a witness: concrete input values that drive execution to it.
+            'stmtIndex' is the statement index from the get_method_ir tool output — call it
+            first to pick the target (e.g. a particular 'return' or a branch of an 'if').
+            Status NOT_REACHED_WITHIN_BUDGET means the directed search failed within the time
+            budget; it is strong evidence but NOT a proof of unreachability.
+        """.trimIndent(),
+        inputSchema = toolSchema(required = listOf("file", "method", "stmtIndex")) {
+            fileProp()
+            classProp()
+            methodProp()
+            intProp("stmtIndex", "Index of the target statement in the method CFG (see get_method_ir).")
+            timeoutProp()
+        },
+    ) { request ->
+        runTool {
+            val args = request.arguments
+            val scene = ctx.scenes.getScene(args.requireStringArg("file"))
+            val method = MethodLookup.findMethod(scene, args.stringArg("class"), args.requireStringArg("method"))
+            val stmts = method.cfg.stmts
+            val stmtIndex = args.intArg("stmtIndex")
+                ?: throw McpToolException("Missing required integer argument 'stmtIndex'.")
+            if (stmtIndex !in stmts.indices) {
+                throw McpToolException(
+                    "stmtIndex $stmtIndex is out of range: method '${method.name}' has ${stmts.size} " +
+                        "statements (valid indices 0..${stmts.size - 1}). Use get_method_ir to list them."
+                )
+            }
+            val target = stmts[stmtIndex]
+            val outcome = ctx.runner.runReachability(scene, method, target, args.timeoutArg())
+            val witness = outcome.witness?.let { case ->
+                case.test?.toTestCaseDto() ?: unresolvedTestCase(case.error ?: "unknown resolution error")
+            }
+            textResult(
+                McpJson.encodeToString(
+                    ReachabilityResultDto(
+                        method = method.qualifiedName(),
+                        stmtIndex = stmtIndex,
+                        statement = target.toString(),
+                        status = if (outcome.reached) "REACHABLE" else "NOT_REACHED_WITHIN_BUDGET",
+                        witness = witness,
+                        note = if (outcome.reached) {
+                            "The witness inputs drive execution to the target statement " +
+                                "according to the symbolic model. The model over-approximates " +
+                                "JavaScript semantics in places; validate the witness by actually " +
+                                "running the method with these inputs (e.g. via node/ts-node)."
+                        } else {
+                            "The target was not reached within the budget. This suggests, " +
+                                "but does not prove, that it is unreachable. Try a larger timeoutMs."
+                        },
+                    )
+                )
+            )
+        }
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindCounterexampleTool.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindCounterexampleTool.kt
new file mode 100644
index 0000000000..419e434683
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindCounterexampleTool.kt
@@ -0,0 +1,73 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import kotlinx.serialization.encodeToString
+import org.usvm.api.TsTestValue
+import org.usvm.mcp.json.CounterexampleResultDto
+import org.usvm.mcp.json.McpJson
+import org.usvm.mcp.json.toTestCaseDto
+import org.usvm.mcp.runTool
+import org.usvm.mcp.scene.MethodLookup
+import org.usvm.mcp.scene.MethodLookup.qualifiedName
+import org.usvm.mcp.textResult
+
+fun Server.registerFindCounterexampleTool(ctx: UsvmToolContext) {
+    addTool(
+        name = "find_counterexample",
+        description = """
+            Tries to FALSIFY a hypothesis about the code. Write a boolean property function in
+            a .ts file yourself, then point this tool at it: symbolic execution searches for
+            inputs on which the property returns false ('counterexamples') or crashes ('crashes').
+
+            Hybrid workflows:
+            - Hypothesis checking: "abs(x) is always >= 0" -> write
+              `function prop(x: number): boolean { return abs(x) >= 0; }` (with 'abs' defined
+              in the same file) and analyze 'prop'.
+            - Equivalence of two implementations (e.g. original vs your refactoring): write
+              `function equiv(x: number): boolean { return f(x) === g(x); }` and analyze 'equiv'.
+
+            The property and everything it calls must live in one .ts file. Verdict
+            NO_COUNTEREXAMPLE_WITHIN_BUDGET is NOT a proof: exploration may have missed paths.
+        """.trimIndent(),
+        inputSchema = toolSchema(required = listOf("file", "method")) {
+            fileProp()
+            classProp()
+            stringProp("method", "Name of the boolean property function to falsify.")
+            timeoutProp()
+        },
+    ) { request ->
+        runTool {
+            val args = request.arguments
+            val scene = ctx.scenes.getScene(args.requireStringArg("file"))
+            val method = MethodLookup.findMethod(scene, args.stringArg("class"), args.requireStringArg("method"))
+            val cases = ctx.runner.runTests(scene, method, args.timeoutArg())
+
+            val tests = cases.mapNotNull { it.test }
+            val counterexamples = tests
+                .filter { (it.returnValue as? TsTestValue.TsBoolean)?.value == false }
+                .map { it.toTestCaseDto() }
+            val crashes = tests
+                .filter { it.returnValue is TsTestValue.TsException }
+                .map { it.toTestCaseDto() }
+
+            textResult(
+                McpJson.encodeToString(
+                    CounterexampleResultDto(
+                        method = method.qualifiedName(),
+                        verdict = if (counterexamples.isNotEmpty()) {
+                            "COUNTEREXAMPLE_FOUND"
+                        } else {
+                            "NO_COUNTEREXAMPLE_WITHIN_BUDGET"
+                        },
+                        counterexamples = counterexamples,
+                        crashes = crashes,
+                        totalPathsExplored = cases.size,
+                        note = "A counterexample gives concrete inputs falsifying the property. " +
+                            "'crashes' are inputs on which the property itself threw. " +
+                            "No counterexample within budget is evidence, not a proof.",
+                    )
+                )
+            )
+        }
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindUnreachableCodeTool.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindUnreachableCodeTool.kt
new file mode 100644
index 0000000000..7807c906d0
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindUnreachableCodeTool.kt
@@ -0,0 +1,74 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import kotlinx.serialization.encodeToString
+import org.usvm.mcp.McpToolException
+import org.usvm.mcp.json.McpJson
+import org.usvm.mcp.json.StmtRefDto
+import org.usvm.mcp.json.UnreachableCodeResultDto
+import org.usvm.mcp.json.UnreachableFindingDto
+import org.usvm.mcp.runTool
+import org.usvm.mcp.scene.MethodLookup
+import org.usvm.mcp.scene.MethodLookup.isAnalyzable
+import org.usvm.mcp.scene.MethodLookup.qualifiedName
+import org.usvm.mcp.textResult
+
+fun Server.registerFindUnreachableCodeTool(ctx: UsvmToolContext) {
+    addTool(
+        name = "find_unreachable_code",
+        description = """
+            Detects likely dead code: branches of 'if' statements that were never taken during
+            symbolic exploration of the given method (or of all methods in the file/class when
+            'method' is omitted). Reports the 'if' statement and its uncovered successor
+            statements (CFG indices, usable with get_method_ir). Findings mean 'uncovered
+            within budget' — verify suspicious ones with check_reachability using a larger budget.
+        """.trimIndent(),
+        inputSchema = toolSchema(required = listOf("file")) {
+            fileProp()
+            classProp()
+            stringProp("method", "Optional method name; when omitted, all analyzable methods are checked.")
+            timeoutProp()
+        },
+    ) { request ->
+        runTool {
+            val args = request.arguments
+            val scene = ctx.scenes.getScene(args.requireStringArg("file"))
+            val methodName = args.stringArg("method")
+            val methods = if (methodName != null) {
+                listOf(MethodLookup.findMethod(scene, args.stringArg("class"), methodName))
+            } else {
+                MethodLookup.findClasses(scene, args.stringArg("class"))
+                    .flatMap { it.methods }
+                    .filter { it.isAnalyzable() }
+            }
+            if (methods.isEmpty()) {
+                throw McpToolException("No analyzable methods found. Use list_methods to inspect the file.")
+            }
+
+            val result = ctx.runner.runUnreachableDetection(scene, methods, args.timeoutArg())
+            val findings = result.flatMap { (method, uncovered) ->
+                val stmts = method.cfg.stmts
+                uncovered.map { finding ->
+                    UnreachableFindingDto(
+                        method = method.qualifiedName(),
+                        ifStmtIndex = stmts.indexOf(finding.ifStmt),
+                        ifStmt = finding.ifStmt.toString(),
+                        uncoveredSuccessors = finding.successors.map { successor ->
+                            StmtRefDto(index = stmts.indexOf(successor), text = successor.toString())
+                        },
+                    )
+                }
+            }
+            textResult(
+                McpJson.encodeToString(
+                    UnreachableCodeResultDto(
+                        findings = findings,
+                        analyzedMethods = methods.map { it.qualifiedName() },
+                        note = "Findings are branches uncovered within the budget, not proofs of unreachability. " +
+                            "Confirm each one with check_reachability on the successor statement index.",
+                    )
+                )
+            )
+        }
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GenerateTestsTool.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GenerateTestsTool.kt
new file mode 100644
index 0000000000..035ec36f1e
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GenerateTestsTool.kt
@@ -0,0 +1,49 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import kotlinx.serialization.encodeToString
+import org.usvm.mcp.json.GenerateTestsResultDto
+import org.usvm.mcp.json.McpJson
+import org.usvm.mcp.json.toTestCaseDto
+import org.usvm.mcp.json.unresolvedTestCase
+import org.usvm.mcp.runTool
+import org.usvm.mcp.scene.MethodLookup
+import org.usvm.mcp.scene.MethodLookup.qualifiedName
+import org.usvm.mcp.textResult
+
+fun Server.registerGenerateTestsTool(ctx: UsvmToolContext) {
+    addTool(
+        name = "generate_tests",
+        description = """
+            Symbolically executes a TypeScript method and returns one concrete test case per
+            explored execution path: input values ('thisInstance' and 'parameters') plus the
+            expected outcome (a return value, or an exception for failing paths).
+            Use the results to write unit tests with real assertions. $BUDGET_NOTE
+        """.trimIndent(),
+        inputSchema = toolSchema(required = listOf("file", "method")) {
+            fileProp()
+            classProp()
+            methodProp()
+            timeoutProp()
+        },
+    ) { request ->
+        runTool {
+            val args = request.arguments
+            val scene = ctx.scenes.getScene(args.requireStringArg("file"))
+            val method = MethodLookup.findMethod(scene, args.stringArg("class"), args.requireStringArg("method"))
+            val cases = ctx.runner.runTests(scene, method, args.timeoutArg())
+            val dtos = cases.map { case ->
+                case.test?.toTestCaseDto() ?: unresolvedTestCase(case.error ?: "unknown resolution error")
+            }
+            textResult(
+                McpJson.encodeToString(
+                    GenerateTestsResultDto(
+                        method = method.qualifiedName(),
+                        testCases = dtos,
+                        note = "Each test case corresponds to a distinct symbolic execution path. $BUDGET_NOTE",
+                    )
+                )
+            )
+        }
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GetMethodIrTool.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GetMethodIrTool.kt
new file mode 100644
index 0000000000..57b655f9d5
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GetMethodIrTool.kt
@@ -0,0 +1,50 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import kotlinx.serialization.encodeToString
+import org.usvm.mcp.json.McpJson
+import org.usvm.mcp.json.MethodIrResultDto
+import org.usvm.mcp.json.StmtDto
+import org.usvm.mcp.runTool
+import org.usvm.mcp.scene.MethodLookup
+import org.usvm.mcp.scene.MethodLookup.qualifiedName
+import org.usvm.mcp.textResult
+
+fun Server.registerGetMethodIrTool(ctx: UsvmToolContext) {
+    addTool(
+        name = "get_method_ir",
+        description = """
+            Shows the control-flow graph (CFG) of a method as a list of IR statements with
+            their indices and successor indices. Source line numbers are NOT available in the IR,
+            so statement 'index' is the only way to address a statement: pass it as 'stmtIndex'
+            to check_reachability. Statements are rendered in an assembly-like form
+            (conditions of 'if' statements, return statements, assignments etc.), which lets you
+            match them back to the source code.
+        """.trimIndent(),
+        inputSchema = toolSchema(required = listOf("file", "method")) {
+            fileProp()
+            classProp()
+            methodProp()
+        },
+    ) { request ->
+        runTool {
+            val args = request.arguments
+            val scene = ctx.scenes.getScene(args.requireStringArg("file"))
+            val method = MethodLookup.findMethod(scene, args.stringArg("class"), args.requireStringArg("method"))
+            val stmts = method.cfg.stmts
+            val statements = stmts.mapIndexed { index, stmt ->
+                StmtDto(
+                    index = index,
+                    kind = stmt::class.simpleName ?: "EtsStmt",
+                    text = stmt.toString(),
+                    successors = method.cfg.successors(stmt).map { stmts.indexOf(it) }.sorted(),
+                )
+            }
+            textResult(
+                McpJson.encodeToString(
+                    MethodIrResultDto(method = method.qualifiedName(), statements = statements)
+                )
+            )
+        }
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ListMethodsTool.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ListMethodsTool.kt
new file mode 100644
index 0000000000..0eb1d426ab
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ListMethodsTool.kt
@@ -0,0 +1,46 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.server.Server
+import kotlinx.serialization.encodeToString
+import org.usvm.mcp.json.ClassDto
+import org.usvm.mcp.json.ListMethodsResultDto
+import org.usvm.mcp.json.McpJson
+import org.usvm.mcp.json.MethodDto
+import org.usvm.mcp.json.ParamDto
+import org.usvm.mcp.runTool
+import org.usvm.mcp.textResult
+
+fun Server.registerListMethodsTool(ctx: UsvmToolContext) {
+    addTool(
+        name = "list_methods",
+        description = """
+            Lists all classes and methods of a TypeScript file that are visible to the USVM
+            symbolic machine. Use it first to discover exact 'class'/'method' argument values
+            for the other tools. Top-level functions are listed under a synthetic default class.
+        """.trimIndent(),
+        inputSchema = toolSchema(required = listOf("file")) {
+            fileProp()
+        },
+    ) { request ->
+        runTool {
+            val file = request.arguments.requireStringArg("file")
+            val scene = ctx.scenes.getScene(file)
+            val classes = scene.projectClasses.map { cls ->
+                ClassDto(
+                    name = cls.name,
+                    methods = cls.methods.map { method ->
+                        MethodDto(
+                            name = method.name,
+                            parameters = method.parameters.map { param ->
+                                ParamDto(name = param.name, type = param.type.toString())
+                            },
+                            returnType = method.returnType.toString(),
+                            stmtCount = runCatching { method.cfg.stmts.size }.getOrDefault(0),
+                        )
+                    },
+                )
+            }
+            textResult(McpJson.encodeToString(ListMethodsResultDto(file = file, classes = classes)))
+        }
+    }
+}
diff --git a/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ToolDefinitions.kt b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ToolDefinitions.kt
new file mode 100644
index 0000000000..e80a593a02
--- /dev/null
+++ b/usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ToolDefinitions.kt
@@ -0,0 +1,84 @@
+package org.usvm.mcp.tools
+
+import io.modelcontextprotocol.kotlin.sdk.types.ToolSchema
+import kotlinx.serialization.json.JsonObject
+import kotlinx.serialization.json.JsonObjectBuilder
+import kotlinx.serialization.json.JsonPrimitive
+import kotlinx.serialization.json.buildJsonObject
+import kotlinx.serialization.json.contentOrNull
+import kotlinx.serialization.json.intOrNull
+import kotlinx.serialization.json.put
+import kotlinx.serialization.json.putJsonObject
+import org.usvm.mcp.McpToolException
+import org.usvm.mcp.exec.TsAnalysisRunner
+import org.usvm.mcp.scene.SceneCache
+import kotlin.time.Duration
+import kotlin.time.Duration.Companion.milliseconds
+
+/** Shared dependencies injected into every tool. */
+class UsvmToolContext(
+    val scenes: SceneCache,
+    val runner: TsAnalysisRunner,
+)
+
+// --- Input schema helpers -------------------------------------------------
+
+fun toolSchema(required: List<String>, block: JsonObjectBuilder.() -> Unit): ToolSchema =
+    ToolSchema(properties = buildJsonObject(block), required = required)
+
+fun JsonObjectBuilder.stringProp(name: String, description: String) {
+    putJsonObject(name) {
+        put("type", "string")
+        put("description", description)
+    }
+}
+
+fun JsonObjectBuilder.intProp(name: String, description: String) {
+    putJsonObject(name) {
+        put("type", "integer")
+        put("description", description)
+    }
+}
+
+const val DEFAULT_TIMEOUT_MS = 30_000
+const val MIN_TIMEOUT_MS = 1_000
+const val MAX_TIMEOUT_MS = 300_000
+
+const val FILE_DESC =
+    "Path to the TypeScript (.ts) source file to analyze " +
+        "(absolute, or relative to the MCP server working directory)."
+
+const val CLASS_DESC =
+    "Optional class name. Omit it for top-level functions or when the method name is unique in the file."
+
+const val METHOD_DESC = "Name of the method/function to analyze."
+
+const val TIMEOUT_DESC =
+    "Analysis budget in milliseconds (default $DEFAULT_TIMEOUT_MS, min $MIN_TIMEOUT_MS, max $MAX_TIMEOUT_MS). " +
+        "Larger budgets explore more paths."
+
+const val BUDGET_NOTE =
+    "Exploration is bounded by a time budget: absence of a result means 'not found within budget', " +
+        "not a proof of absence."
+
+fun JsonObjectBuilder.fileProp() = stringProp("file", FILE_DESC)
+fun JsonObjectBuilder.classProp() = stringProp("class", CLASS_DESC)
+fun JsonObjectBuilder.methodProp() = stringProp("method", METHOD_DESC)
+fun JsonObjectBuilder.timeoutProp() = intProp("timeoutMs", TIMEOUT_DESC)
+
+// --- Argument extraction --------------------------------------------------
+
+fun JsonObject?.stringArg(name: String): String? =
+    (this?.get(name) as? JsonPrimitive)?.contentOrNull
+
+fun JsonObject?.requireStringArg(name: String): String =
+    stringArg(name)
+        ?: throw McpToolException("Missing required string argument '$name'.")
+
+fun JsonObject?.intArg(name: String): Int? =
+    (this?.get(name) as? JsonPrimitive)?.intOrNull
+
+fun JsonObject?.timeoutArg(): Duration {
+    val ms = intArg("timeoutMs") ?: DEFAULT_TIMEOUT_MS
+    return ms.coerceIn(MIN_TIMEOUT_MS, MAX_TIMEOUT_MS).milliseconds
+}
diff --git a/usvm-mcp/src/main/resources/logback.xml b/usvm-mcp/src/main/resources/logback.xml
new file mode 100644
index 0000000000..943944ff08
--- /dev/null
+++ b/usvm-mcp/src/main/resources/logback.xml
@@ -0,0 +1,21 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<configuration>
+    <!-- stdout is the MCP JSON-RPC channel: all logging must go to stderr. -->
+    <appender name="STDERR" class="ch.qos.logback.core.ConsoleAppender">
+        <target>System.err</target>
+        <encoder>
+            <pattern>%d{HH:mm:ss.SSS} %-5level %logger{24} - %msg%n</pattern>
+        </encoder>
+    </appender>
+
+    <!-- The symbolic machine is chatty; keep only warnings. -->
+    <logger name="org.usvm" level="WARN"/>
+    <logger name="org.jacodb" level="WARN"/>
+    <logger name="io.ksmt" level="WARN"/>
+    <!-- But keep the MCP server's own messages. -->
+    <logger name="org.usvm.mcp" level="INFO"/>
+
+    <root level="INFO">
+        <appender-ref ref="STDERR"/>
+    </root>
+</configuration>
diff --git a/usvm-mcp/src/test/kotlin/org/usvm/mcp/TsTestValueJsonTest.kt b/usvm-mcp/src/test/kotlin/org/usvm/mcp/TsTestValueJsonTest.kt
new file mode 100644
index 0000000000..9c47bc1877
--- /dev/null
+++ b/usvm-mcp/src/test/kotlin/org/usvm/mcp/TsTestValueJsonTest.kt
@@ -0,0 +1,67 @@
+package org.usvm.mcp
+
+import kotlinx.serialization.json.JsonNull
+import kotlinx.serialization.json.JsonPrimitive
+import kotlinx.serialization.json.jsonArray
+import kotlinx.serialization.json.jsonObject
+import kotlinx.serialization.json.jsonPrimitive
+import org.usvm.api.TsTestValue
+import org.usvm.mcp.json.toExceptionDto
+import org.usvm.mcp.json.toJson
+import kotlin.test.Test
+import kotlin.test.assertEquals
+
+class TsTestValueJsonTest {
+
+    @Test
+    fun `primitives map to json primitives`() {
+        assertEquals(JsonPrimitive(true), TsTestValue.TsBoolean(true).toJson())
+        assertEquals(JsonPrimitive(42), TsTestValue.TsNumber.TsInteger(42).toJson())
+        assertEquals(JsonPrimitive(3.5), TsTestValue.TsNumber.TsDouble(3.5).toJson())
+        assertEquals(JsonPrimitive("hi"), TsTestValue.TsString("hi").toJson())
+        assertEquals(JsonNull, TsTestValue.TsNull.toJson())
+    }
+
+    @Test
+    fun `undefined is a tagged object`() {
+        val json = TsTestValue.TsUndefined.toJson().jsonObject
+        assertEquals("undefined", json.getValue("\$kind").jsonPrimitive.content)
+    }
+
+    @Test
+    fun `objects keep class name and properties`() {
+        val obj = TsTestValue.TsClass(
+            name = "Point",
+            properties = mapOf(
+                "x" to TsTestValue.TsNumber.TsInteger(1),
+                "y" to TsTestValue.TsNumber.TsDouble(2.0),
+            ),
+        )
+        val json = obj.toJson().jsonObject
+        assertEquals("object", json.getValue("\$kind").jsonPrimitive.content)
+        assertEquals("Point", json.getValue("class").jsonPrimitive.content)
+        val props = json.getValue("properties").jsonObject
+        assertEquals(JsonPrimitive(1), props.getValue("x"))
+        assertEquals(JsonPrimitive(2.0), props.getValue("y"))
+    }
+
+    @Test
+    fun `arrays are json arrays`() {
+        val arr = TsTestValue.TsArray(
+            listOf(TsTestValue.TsNumber.TsInteger(1), TsTestValue.TsNumber.TsInteger(2)),
+        )
+        val json = arr.toJson().jsonArray
+        assertEquals(2, json.size)
+        assertEquals(JsonPrimitive(1), json[0])
+    }
+
+    @Test
+    fun `exceptions carry type and message`() {
+        val dto = TsTestValue.TsException.StringException("boom").toExceptionDto()
+        assertEquals("string", dto.type)
+        assertEquals("boom", dto.message)
+
+        val unknown = TsTestValue.TsException.UnknownException.toExceptionDto()
+        assertEquals("unknown", unknown.type)
+    }
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ObjectClass.kt
similarity index 100%
rename from usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt
rename to usvm-ts/src/main/kotlin/org/usvm/util/ObjectClass.kt
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt
similarity index 100%
rename from usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
rename to usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt