diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
new file mode 100644
index 0000000000..5f1d3f0971
--- /dev/null
+++ b/.devcontainer/Dockerfile
@@ -0,0 +1,26 @@
+# Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+# Authors: Fabrizio Montesi
+
+FROM mcr.microsoft.com/devcontainers/base:ubuntu
+
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    build-essential \
+    ca-certificates \
+    curl \
+    ripgrep \
+    && rm -rf /var/lib/apt/lists/*
+
+# Install uv + uvx globally for Python CLI tooling (e.g., lean-lsp-mcp).
+RUN curl -LsSf https://astral.sh/uv/install.sh | env UV_INSTALL_DIR=/usr/local/bin sh
+
+USER vscode
+WORKDIR /home/vscode
+
+ENV PATH="/home/vscode/.elan/bin:/home/vscode/.local/bin:${PATH}"
+
+# Install elan
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# Install the Lean LSP MCP server
+RUN uv tool install lean-lsp-mcp
diff --git a/.devcontainer/devcontainer-lock.json b/.devcontainer/devcontainer-lock.json
new file mode 100644
index 0000000000..9b3c0997ad
--- /dev/null
+++ b/.devcontainer/devcontainer-lock.json
@@ -0,0 +1,9 @@
+{
+  "features": {
+    "ghcr.io/devcontainers/features/github-cli:1": {
+      "version": "1.1.2",
+      "resolved": "ghcr.io/devcontainers/features/github-cli@sha256:7c409bf6316ffd85f04fd92fba85a744282639e603417dd4796409866bdb6805",
+      "integrity": "sha256:7c409bf6316ffd85f04fd92fba85a744282639e603417dd4796409866bdb6805"
+    }
+  }
+}
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
new file mode 100644
index 0000000000..f89ecf7dae
--- /dev/null
+++ b/.devcontainer/devcontainer.json
@@ -0,0 +1,22 @@
+{
+  "name": "CSLib Devcontainer",
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
+  "postCreateCommand": "lake exe cache get && lake build",
+  "remoteUser": "vscode",
+  "mounts": [
+    "source=cslib-elan-toolchains,target=/home/vscode/.elan/toolchains,type=volume",
+    "source=cslib-cache,target=/home/vscode/.cache,type=volume"
+  ],
+  "features": {
+    "ghcr.io/devcontainers/features/github-cli:1": {}
+  },
+  "customizations": {
+    "vscode": {
+      "extensions": [
+        "leanprover.lean4"
+      ]
+    }
+  }
+}
diff --git a/scripts/README.md b/scripts/README.md
index 19d71dfa67..f1faeb1032 100644
--- a/scripts/README.md
+++ b/scripts/README.md
@@ -10,6 +10,19 @@ to learn about it as well!
 - `gendocs.sh`
   Generates the documentation for cslib using `lake`.
 
+**Devcontainer helpers**
+- `setup-mistral-vibe.sh`
+  Installs the Mistral Vibe VS Code extension (`mistralai.mistral-vibe-code`) if
+  missing and ensures required Mistral config entries for the `lean` agent and the `lean-lsp` MCP server are present.
+
+  **Usage:**
+  ```bash
+  ./scripts/setup-mistral-vibe.sh
+  ```
+
+  **Optional environment variable:**
+  - `MISTRAL_CONFIG_FILE`: Override the path to `config.toml`.
+
 **Managing nightly-testing and bump branches**
 - `create-adaptation-pr.sh` is a variant of the script from Batteries and implements some of the steps
   in the workflow for managing nightly and bump branches.
diff --git a/scripts/setup-mistral-vibe.sh b/scripts/setup-mistral-vibe.sh
new file mode 100755
index 0000000000..f01d106a30
--- /dev/null
+++ b/scripts/setup-mistral-vibe.sh
@@ -0,0 +1,115 @@
+#!/usr/bin/env bash
+
+# Configure Mistral Vibe for this development environment.
+# - Installs the Mistral Vibe VS Code extension if missing.
+# - Ensures required TOML entries exist in the Mistral config file.
+
+set -euo pipefail
+IFS=$'\n\t'
+
+log() {
+  echo "[setup-mistral-vibe] $*"
+}
+
+error() {
+  echo "[setup-mistral-vibe] ERROR: $*" >&2
+}
+
+ensure_code_cli() {
+  if ! command -v code >/dev/null 2>&1; then
+    error "The 'code' CLI is not available in PATH."
+    error "In VS Code, run: Command Palette -> 'Shell Command: Install code command in PATH'."
+    exit 1
+  fi
+}
+
+resolve_config_file() {
+  if [ -n "${MISTRAL_CONFIG_FILE:-}" ]; then
+    echo "$MISTRAL_CONFIG_FILE"
+    return
+  fi
+
+  echo "$HOME/.vibe/config.toml"
+}
+
+install_vibe_vscode_extension_if_missing() {
+  local extension_id="mistralai.mistral-vibe-code"
+
+  if code --list-extensions | grep -Fxq "$extension_id"; then
+    log "VS Code extension '$extension_id' is already installed."
+    return
+  fi
+
+  log "Installing VS Code extension '$extension_id'..."
+  code --install-extension "$extension_id"
+  log "Installed VS Code extension '$extension_id'."
+}
+
+ensure_installed_agents_contains_lean() {
+  local config_file=$1
+
+  perl -0777 -i -pe '
+    my $added = 0;
+    if (/^\s*installed_agents\s*=\s*\[(.*?)\]/ms) {
+      my $block = $&;
+      my $items = $1;
+      if ($items !~ /"lean"/) {
+        my $replacement = $block;
+        if ($replacement =~ /\[\s*\]/s) {
+          $replacement =~ s/\[\s*\]/[\n    "lean",\n]/s;
+        } else {
+          $replacement =~ s/\]\s*$/    "lean",\n]/s;
+        }
+        s/\Q$block\E/$replacement/s;
+        $added = 1;
+      }
+    } else {
+      $_ .= "\ninstalled_agents = [\n    \"lean\",\n]\n";
+      $added = 1;
+    }
+    END {
+      if ($added) {
+        print STDERR "[setup-mistral-vibe] Added installed_agents entry for lean.\n";
+      }
+    }
+  ' "$config_file"
+}
+
+ensure_lean_lsp_mcp_server() {
+  local config_file=$1
+
+  if grep -Eq '^[[:space:]]*name[[:space:]]*=[[:space:]]*"lean-lsp"' "$config_file"; then
+    log "lean-lsp MCP server already configured."
+    return
+  fi
+
+  cat >>"$config_file" <<'EOF'
+
+[[mcp_servers]]
+name = "lean-lsp"
+transport = "stdio"
+command = "uvx"
+args = [
+    "lean-lsp-mcp",
+]
+tool_timeout_sec = 600
+EOF
+  log "Added lean-lsp MCP server configuration."
+}
+
+main() {
+  ensure_code_cli
+  install_vibe_vscode_extension_if_missing
+
+  local config_file
+  config_file=$(resolve_config_file)
+  mkdir -p "$(dirname "$config_file")"
+  touch "$config_file"
+
+  ensure_installed_agents_contains_lean "$config_file"
+  ensure_lean_lsp_mcp_server "$config_file"
+
+  log "Setup complete. Config updated at: $config_file"
+}
+
+main "$@"
\ No newline at end of file