diff --git a/client/.vscodeignore b/client/.vscodeignore
index d42f18e5..fcc43ef2 100644
--- a/client/.vscodeignore
+++ b/client/.vscodeignore
@@ -26,6 +26,7 @@ test/**
 *.md
 !README.md
 !USAGE.md
+!media/walkthrough/*.md
 
 # Source maps (comment out if you want to include them)
 **/*.map
diff --git a/client/README.md b/client/README.md
index 3564a915..7b359afc 100644
--- a/client/README.md
+++ b/client/README.md
@@ -38,6 +38,10 @@ dependencies {
 
 A repository with LiquidJava examples is available at [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples). You can try them out without setting up your local environment using [GitHub Codespaces](https://codespaces.new/liquid-java/liquidjava-examples).
 
+### Getting started in VS Code
+
+The **Get Started with LiquidJava** walkthrough introduces LiquidJava and its interactive tutorial, includes copyable Maven/Gradle annotation dependencies, then explains verification and its status indicator, diagnostics, context, state machines, the Command Palette, and logs. It also links to the [interactive tutorial](https://liquid-java.github.io/liquidjava-interactive-tutorial/). It opens once on installation, following VS Code’s walkthrough preferences. You can dismiss it at any time and reopen it with **LiquidJava: Show Walkthrough** from the Command Palette or **LiquidJava: Show Commands**. VS Code saves its progress across workspaces.
+
 ### What are Liquid Types?
 
 Liquid types extend a language with **logical predicates** over the basic types. They allow developers to restrict the values that a variable, parameter or return value can have. These kinds of constraints help to catch more bugs before the program is executed. For example, they allow us to prevent bugs like array index out-of-bounds or division by zero at compile-time.
@@ -138,4 +142,4 @@ For more information, check the following repositories:
 - [vscode-liquidjava](https://github.com/liquid-java/vscode-liquidjava): Source code of this VS Code extension
 - [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples): Examples of how to use LiquidJava
 - [liquid-java-external-libs](https://github.com/liquid-java/liquid-java-external-libs): Examples of how to use LiquidJava to refine external libraries
-- [liquidjava-fsm](https://github.com/liquid-java/liquidjava-fsm): State machine parser used by the VS Code language server
\ No newline at end of file
+- [liquidjava-fsm](https://github.com/liquid-java/liquidjava-fsm): State machine parser used by the VS Code language server
diff --git a/client/media/walkthrough/annotations.md b/client/media/walkthrough/annotations.md
new file mode 100644
index 00000000..b88406ee
--- /dev/null
+++ b/client/media/walkthrough/annotations.md
@@ -0,0 +1,23 @@
+## Maven — `pom.xml`
+
+```xml
+<dependency>
+    <groupId>io.github.liquid-java</groupId>
+    <artifactId>liquidjava-api</artifactId>
+    <version>0.0.7</version>
+</dependency>
+```
+
+## Gradle — `build.gradle`
+
+```groovy
+repositories {
+    mavenCentral()
+}
+
+dependencies {
+    implementation 'io.github.liquid-java:liquidjava-api:0.0.7'
+}
+```
+
+Reload your Java project after changing dependencies. Import annotations from `liquidjava.specification`, for example `liquidjava.specification.Refinement`.
diff --git a/client/media/walkthrough/commands.md b/client/media/walkthrough/commands.md
new file mode 100644
index 00000000..231fc5c4
--- /dev/null
+++ b/client/media/walkthrough/commands.md
@@ -0,0 +1,5 @@
+# LiquidJava commands
+
+Click the status indicator or **Show LiquidJava commands** to open the LiquidJava-only command list.
+
+Use **Start**, **Stop**, or **Restart** to control the verifier. Run **Verify** after returning to a Java editor.
diff --git a/client/media/walkthrough/context.md b/client/media/walkthrough/context.md
new file mode 100644
index 00000000..4b8349ff
--- /dev/null
+++ b/client/media/walkthrough/context.md
@@ -0,0 +1,3 @@
+The **Context** tab shows **Variables**, **Aliases**, and **Ghosts** after verification. Expand or collapse each section.
+Local variables are filtered by the cursor: only declarations before it and in enclosing scopes appear. Select a range to inspect declarations that overlap it; global variables are also included.
+Click a variable to reveal its source. Variables relevant to a nearby error are highlighted alongside the failing refinement.
diff --git a/client/media/walkthrough/diagnostics.md b/client/media/walkthrough/diagnostics.md
new file mode 100644
index 00000000..410e36a7
--- /dev/null
+++ b/client/media/walkthrough/diagnostics.md
@@ -0,0 +1,3 @@
+The **Verification** tab compares **Found** with **Expected**. Click a location or variable to jump to its source.
+When a simplification history is available, use **Previous simplification** and **Next simplification** to inspect highlighted changes. Inspect a **Hint** or **Counterexample** when available.
+Switch between **Current file** and **Workspace**, or use **View related context** and **View error on state machine** to investigate an error.
diff --git a/client/media/walkthrough/logs.md b/client/media/walkthrough/logs.md
new file mode 100644
index 00000000..e979b633
--- /dev/null
+++ b/client/media/walkthrough/logs.md
@@ -0,0 +1,5 @@
+# Inspect the logger
+
+Run **LiquidJava: Show Logs** to open the **LiquidJava** output channel.
+
+Entries include a timestamp, **CLIENT** or **SERVER** source, and **INFO** or **ERROR** level.
diff --git a/client/media/walkthrough/state-machine.md b/client/media/walkthrough/state-machine.md
new file mode 100644
index 00000000..a12bc4bb
--- /dev/null
+++ b/client/media/walkthrough/state-machine.md
@@ -0,0 +1,4 @@
+The **State Machine** tab shows object states and method transitions declared with `@StateSet` and `@StateRefinement`.
+Pan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.
+Use **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.
+From a state error, choose **View error on state machine** to see the related states and call.
diff --git a/client/media/walkthrough/tutorial.md b/client/media/walkthrough/tutorial.md
new file mode 100644
index 00000000..e7ff5325
--- /dev/null
+++ b/client/media/walkthrough/tutorial.md
@@ -0,0 +1,5 @@
+# Learn LiquidJava
+
+LiquidJava is an additional type checker for Java, based on **liquid types** and **typestates**, which provides stronger safety guarantees to Java programs at compile-time.
+
+Edit short Java examples and run verification in the browser with the interactive tutorial. No local setup needed.
diff --git a/client/media/walkthrough/verification.md b/client/media/walkthrough/verification.md
new file mode 100644
index 00000000..45d6d013
--- /dev/null
+++ b/client/media/walkthrough/verification.md
@@ -0,0 +1,8 @@
+# Read the status indicator
+
+- **Spinning arrows:** checking your code.
+- **Check mark:** verification passed.
+- **Cross:** verification failed or the verifier crashed.
+- **Slashed circle:** verifier stopped.
+
+Hover for details. Click the indicator to open LiquidJava commands.
diff --git a/client/package.json b/client/package.json
index b5891b5b..814ca377 100644
--- a/client/package.json
+++ b/client/package.json
@@ -92,6 +92,11 @@
 				"title": "Show Commands",
 				"category": "LiquidJava"
 			},
+			{
+				"command": "liquidjava.showWalkthrough",
+				"title": "Show Walkthrough",
+				"category": "LiquidJava"
+			},
 			{
 				"command": "liquidjava.showLogs",
 				"title": "Show Logs",
@@ -125,6 +130,16 @@
 				"command": "liquidjava.verify",
 				"title": "Verify",
 				"category": "LiquidJava"
+			},
+			{
+				"command": "liquidjava.copyMavenDependency",
+				"title": "Copy Maven Dependency",
+				"category": "LiquidJava"
+			},
+			{
+				"command": "liquidjava.copyGradleDependency",
+				"title": "Copy Gradle Dependency",
+				"category": "LiquidJava"
 			}
 		],
 		"menus": {
@@ -149,7 +164,104 @@
 			"[java]": {
 				"editor.autoClosingBrackets": "always"
 			}
-		}
+		},
+		"walkthroughs": [
+			{
+				"id": "getStarted",
+				"title": "Get Started with LiquidJava",
+				"description": "Learn LiquidJava, add annotations, and discover verification, views, commands, and logs.",
+				"steps": [
+					{
+						"id": "tutorial",
+						"title": "Learn LiquidJava",
+						"description": "LiquidJava is an additional type checker for Java, based on **liquid types** and **typestates**, which provides stronger safety guarantees to Java programs at compile-time.\nLearn refinements, method contracts, object states, and ghost variables with short examples in the interactive tutorial.\n[Open interactive tutorial](https://liquid-java.github.io/liquidjava-interactive-tutorial/)",
+						"media": {
+							"markdown": "media/walkthrough/tutorial.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					},
+					{
+						"id": "annotations",
+						"title": "Add the annotation API",
+						"description": "Add ``liquidjava-api`` to your project to use annotations such as ``@Refinement``.\n**Maven — pom.xml**\n``<dependency>``\n``    <groupId>io.github.liquid-java</groupId>``\n``    <artifactId>liquidjava-api</artifactId>``\n``    <version>0.0.7</version>``\n``</dependency>``\n[Copy Maven dependency](command:liquidjava.copyMavenDependency)\n**Gradle — build.gradle**\n``repositories {``\n``    mavenCentral()``\n``}``\n``dependencies {``\n``    implementation 'io.github.liquid-java:liquidjava-api:0.0.7'``\n``}``\n[Copy Gradle dependency](command:liquidjava.copyGradleDependency)\nReload the Java project after changing dependencies. Import annotations from ``liquidjava.specification``.",
+						"media": {
+							"markdown": "media/walkthrough/annotations.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					},
+					{
+						"id": "verification",
+						"title": "Verification and status",
+						"description": "Open or save a Java file to verify it. Watch the **LiquidJava** indicator in the bottom status bar.\nA spinner means checking; a check mark means passed; a cross means failed or crashed; a slashed circle means stopped. Hover for details or click for LiquidJava commands.",
+						"media": {
+							"markdown": "media/walkthrough/verification.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					},
+					{
+						"id": "commands",
+						"title": "Find LiquidJava commands",
+						"description": "Use the status indicator or **Show LiquidJava commands** below to list only LiquidJava actions.\nChoose **Start**, **Stop**, or **Restart** to control the verifier. Use **Verify** after returning to a Java editor. You can also press **F1** and search for LiquidJava in the Command Palette.\n[Show LiquidJava commands](command:liquidjava.showCommands)",
+						"media": {
+							"markdown": "media/walkthrough/commands.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					},
+					{
+						"id": "diagnostics",
+						"title": "Understand diagnostics",
+						"description": "The **Verification** tab compares **Found** with **Expected**. Click a location or variable to jump to its source.\nWhen a simplification history is available, use **Previous simplification** and **Next simplification** to inspect highlighted changes. Inspect a **Hint** or **Counterexample** when available.\nSwitch between **Current file** and **Workspace**, or use **View related context** and **View error on state machine** to investigate an error.\n[Open LiquidJava view](command:liquidjava.showView)",
+						"media": {
+							"markdown": "media/walkthrough/diagnostics.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					},
+					{
+						"id": "context",
+						"title": "Inspect context",
+						"description": "The **Context** tab shows **Variables**, **Aliases**, and **Ghosts** after verification. Expand or collapse each section.\nLocal variables are filtered by the cursor: only declarations before it and in enclosing scopes appear. Select a range to inspect declarations that overlap it; global variables are also included.\nClick a variable to reveal its source. Variables relevant to a nearby error are highlighted alongside the failing refinement.\n[Open LiquidJava view](command:liquidjava.showView)",
+						"media": {
+							"markdown": "media/walkthrough/context.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					},
+					{
+						"id": "stateMachine",
+						"title": "Explore state machines",
+						"description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **View error on state machine** to see the related states and call.\n[Open LiquidJava view](command:liquidjava.showView)",
+						"media": {
+							"markdown": "media/walkthrough/state-machine.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					},
+					{
+						"id": "logs",
+						"title": "Check the logs",
+						"description": "The **LiquidJava** output channel records extension and verifier activity. Use it to investigate startup or verification problems.\nEach entry includes a timestamp, **CLIENT** or **SERVER** source, and **INFO** or **ERROR** level.\n[Show LiquidJava logs](command:liquidjava.showLogs)",
+						"media": {
+							"markdown": "media/walkthrough/logs.md"
+						},
+						"completionEvents": [
+							"onStepSelected"
+						]
+					}
+				]
+			}
+		]
 	},
 	"scripts": {
 		"vscode:prepublish": "npm run package",
diff --git a/client/src/services/commands.ts b/client/src/services/commands.ts
index 9998b151..61fd0268 100644
--- a/client/src/services/commands.ts
+++ b/client/src/services/commands.ts
@@ -1,10 +1,14 @@
 import * as vscode from "vscode";
 import { startExtension, stopExtension, restartExtension } from "../extension";
 import { verify } from "./diagnostics";
+import { copyWalkthroughDependency, showWalkthrough } from './walkthrough';
 
 const commandIcons: Record<string, string> = {
     "liquidjava.showLogs": "$(output)",
     "liquidjava.showView": "$(window)",
+    "liquidjava.showWalkthrough": "$(book)",
+    "liquidjava.copyMavenDependency": "$(copy)",
+    "liquidjava.copyGradleDependency": "$(copy)",
     "liquidjava.start": "$(play)",
     "liquidjava.stop": "$(debug-stop)",
     "liquidjava.restart": "$(debug-restart)",
@@ -12,6 +16,9 @@ const commandIcons: Record<string, string> = {
 };
 
 const commandHandlers: Record<string, (context: vscode.ExtensionContext) => Promise<void>> = {
+    "liquidjava.showWalkthrough": showWalkthrough,
+    "liquidjava.copyMavenDependency": async context => await copyWalkthroughDependency(context, 'xml'),
+    "liquidjava.copyGradleDependency": async context => await copyWalkthroughDependency(context, 'groovy'),
     "liquidjava.start": async (context) => await startExtension(context),
     "liquidjava.stop": async () => await stopExtension(),
     "liquidjava.restart": async (context) => await restartExtension(context),
@@ -51,4 +58,4 @@ export function registerCommands(context: vscode.ExtensionContext) {
             if (selected) vscode.commands.executeCommand(selected.command);
         })
     );    
-}
\ No newline at end of file
+}
diff --git a/client/src/services/walkthrough.ts b/client/src/services/walkthrough.ts
new file mode 100644
index 00000000..e9661285
--- /dev/null
+++ b/client/src/services/walkthrough.ts
@@ -0,0 +1,16 @@
+import * as vscode from 'vscode';
+
+export const WALKTHROUGH_ID = 'AlcidesFonseca.liquid-java#getStarted';
+
+export async function showWalkthrough(): Promise<void> {
+    await vscode.commands.executeCommand('workbench.action.openWalkthrough', WALKTHROUGH_ID);
+}
+
+export async function copyWalkthroughDependency(context: Pick<vscode.ExtensionContext, 'extensionUri'>, language: 'xml' | 'groovy'): Promise<void> {
+    const uri = vscode.Uri.joinPath(context.extensionUri, 'media/walkthrough/annotations.md');
+    const contents = Buffer.from(await vscode.workspace.fs.readFile(uri)).toString('utf8').replace(/\r\n/g, '\n');
+    const snippet = contents.match(new RegExp('```' + language + '\\n([\\s\\S]*?)\\n```'))?.[1];
+    if (!snippet) throw new Error('LiquidJava walkthrough dependency snippet is missing');
+    await vscode.env.clipboard.writeText(snippet);
+    vscode.window.setStatusBarMessage('LiquidJava: ' + (language === 'xml' ? 'Maven' : 'Gradle') + ' dependency copied', 3000);
+}
diff --git a/client/src/test/walkthrough.test.ts b/client/src/test/walkthrough.test.ts
new file mode 100644
index 00000000..9270f5b0
--- /dev/null
+++ b/client/src/test/walkthrough.test.ts
@@ -0,0 +1,121 @@
+import * as assert from 'node:assert/strict';
+import { mkdir, mkdtemp, readFile, rm, writeFile } from 'node:fs/promises';
+import { tmpdir } from 'node:os';
+import { join } from 'node:path';
+import * as vscode from 'vscode';
+import { copyWalkthroughDependency, WALKTHROUGH_ID } from '../services/walkthrough';
+import type { LiquidJavaTestApi } from '../types/test-api';
+
+suite('LiquidJava walkthrough', () => {
+    let installed: vscode.Extension<LiquidJavaTestApi>;
+
+    suiteSetup(async () => {
+        installed = vscode.extensions.getExtension<LiquidJavaTestApi>('AlcidesFonseca.liquid-java')!;
+        assert.ok(installed);
+        await installed.activate();
+    });
+
+    teardown(async () => {
+        await vscode.commands.executeCommand('workbench.action.closeAllEditors');
+    });
+
+    test('contributes the tour with readable content and usable actions', async () => {
+        const walkthrough = installed.packageJSON.contributes.walkthroughs.find(
+            (entry: { id: string }) => `${installed.id}#${entry.id}` === WALKTHROUGH_ID);
+        assert.ok(walkthrough);
+        assert.equal(walkthrough.title, 'Get Started with LiquidJava');
+        assert.deepEqual(walkthrough.steps.map((step: { id: string }) => step.id),
+            ['tutorial', 'annotations', 'verification', 'commands', 'diagnostics', 'context', 'stateMachine', 'logs']);
+        assert.equal(walkthrough.steps[0].title, 'Learn LiquidJava');
+        const commands = await vscode.commands.getCommands(true);
+        assert.ok(commands.includes('liquidjava.showWalkthrough'));
+        for (const step of walkthrough.steps) {
+            const content = await readFile(vscode.Uri.joinPath(installed.extensionUri, step.media.markdown).fsPath, 'utf8');
+            assert.ok(content.trim(), `${step.id} must have readable content`);
+            const links = [...step.description.matchAll(/\]\(command:([^)?]+)\)/g)];
+            for (const link of links) assert.ok(commands.includes(link[1]), `unregistered action: ${link[1]}`);
+            assert.ok(!links.some(link => link[1] === 'liquidjava.verify'),
+                'walkthrough actions must work without an active Java editor');
+        }
+        const description = (id: string) => walkthrough.steps.find((step: { id: string }) => step.id === id).description;
+        assert.ok(description('commands').includes('(command:liquidjava.showCommands)'));
+        assert.ok(description('logs').includes('(command:liquidjava.showLogs)'));
+        assert.ok(description('tutorial').includes('(https://liquid-java.github.io/liquidjava-interactive-tutorial/)'));
+    });
+
+    test('uses the README dependency snippets for Maven and Gradle setup', async () => {
+        const readme = (await readFile(vscode.Uri.joinPath(installed.extensionUri, 'README.md').fsPath, 'utf8')).replace(/\r\n/g, '\n');
+        const setup = (await readFile(vscode.Uri.joinPath(installed.extensionUri, 'media/walkthrough/annotations.md').fsPath, 'utf8')).replace(/\r\n/g, '\n');
+        const description = installed.packageJSON.contributes.walkthroughs[0].steps.find(
+            (step: { id: string }) => step.id === 'annotations').description as string;
+        for (const language of ['xml', 'groovy']) {
+            const snippet = readme.match(new RegExp('```' + language + '\\n[\\s\\S]*?```'))?.[0];
+            assert.ok(snippet, `README must include the ${language} dependency snippet`);
+            assert.ok(setup.includes(snippet), `walkthrough ${language} dependency must match the README`);
+            for (const line of snippet.split('\n').slice(1, -1).filter(line => line.trim())) {
+                assert.ok(description.includes('``' + line + '``'),
+                    'dependency code must also appear in the step when VS Code hides its media pane');
+            }
+        }
+        assert.ok(setup.includes('liquidjava.specification.Refinement'));
+    });
+
+    test('copies complete Maven and Gradle snippets from the walkthrough', async () => {
+        const originalClipboard = await vscode.env.clipboard.readText();
+        try {
+            const readme = (await readFile(vscode.Uri.joinPath(installed.extensionUri, 'README.md').fsPath, 'utf8')).replace(/\r\n/g, '\n');
+            await vscode.commands.executeCommand('workbench.action.closeAllEditors');
+            await vscode.commands.executeCommand('liquidjava.showWalkthrough');
+            assert.equal(vscode.window.activeTextEditor, undefined);
+            for (const [language, command] of [
+                ['xml', 'liquidjava.copyMavenDependency'],
+                ['groovy', 'liquidjava.copyGradleDependency'],
+            ]) {
+                const snippet = readme.match(new RegExp('```' + language + '\\n([\\s\\S]*?)\\n```'))?.[1];
+                assert.ok(snippet);
+                await vscode.commands.executeCommand(command);
+                assert.equal(await vscode.env.clipboard.readText(), snippet,
+                    'copy must preserve the complete README snippet and its newlines');
+            }
+        } finally {
+            await vscode.env.clipboard.writeText(originalClipboard);
+        }
+    });
+
+    test('copies dependency snippets from Windows line endings', async () => {
+        const originalClipboard = await vscode.env.clipboard.readText();
+        const directory = await mkdtemp(join(tmpdir(), 'liquidjava-walkthrough-'));
+        try {
+            const source = (await readFile(vscode.Uri.joinPath(installed.extensionUri, 'media/walkthrough/annotations.md').fsPath, 'utf8')).replace(/\r\n/g, '\n');
+            const mediaDirectory = join(directory, 'media', 'walkthrough');
+            await mkdir(mediaDirectory, { recursive: true });
+            await writeFile(join(mediaDirectory, 'annotations.md'), source.replace(/\n/g, '\r\n'));
+            for (const language of ['xml', 'groovy'] as const) {
+                await copyWalkthroughDependency({ extensionUri: vscode.Uri.file(directory) }, language);
+                const expected = source.match(new RegExp('```' + language + '\\n([\\s\\S]*?)\\n```'))?.[1];
+                assert.ok(expected);
+                assert.equal(await vscode.env.clipboard.readText(), expected);
+            }
+        } finally {
+            await vscode.env.clipboard.writeText(originalClipboard);
+            await rm(directory, { recursive: true, force: true });
+        }
+    });
+
+    test('reopens the native walkthrough repeatedly after dismissal', async () => {
+        await vscode.commands.executeCommand('workbench.action.closeAllEditors');
+        await vscode.commands.executeCommand('liquidjava.showWalkthrough');
+        assert.ok(vscode.window.tabGroups.activeTabGroup.activeTab, 'the registered command must reopen the walkthrough');
+        await vscode.commands.executeCommand('workbench.action.closeAllEditors');
+        await vscode.commands.executeCommand('liquidjava.showWalkthrough');
+        assert.ok(vscode.window.tabGroups.activeTabGroup.activeTab, 'manual reopening must remain available');
+    });
+
+    test('opens the logs from the walkthrough without an active Java editor', async () => {
+        await vscode.commands.executeCommand('workbench.action.closeAllEditors');
+        await vscode.commands.executeCommand('liquidjava.showWalkthrough');
+        assert.equal(vscode.window.activeTextEditor, undefined);
+        await vscode.commands.executeCommand('liquidjava.showLogs');
+        assert.ok(vscode.window.tabGroups.activeTabGroup.activeTab, 'opening logs must keep the walkthrough available');
+    });
+});