diff --git a/.claude/settings.json b/.claude/settings.json
new file mode 100644
index 0000000000..b7067fce0f
--- /dev/null
+++ b/.claude/settings.json
@@ -0,0 +1,11 @@
+{
+  "mcpServers": {
+    "github": {
+      "command": "npx",
+      "args": [
+        "-y",
+        "@modelcontextprotocol/server-github"
+      ]
+    }
+  }
+}
diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
new file mode 100644
index 0000000000..df90fe1a05
--- /dev/null
+++ b/.devcontainer/Dockerfile
@@ -0,0 +1,53 @@
+FROM ubuntu:24.04
+
+ARG DEBIAN_FRONTEND=noninteractive
+
+# Install base dependencies
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    curl wget git ca-certificates unzip python3 python3-pip pipx \
+    && rm -rf /var/lib/apt/lists/*
+
+# Install Node.js (needed for Claude Code and Kiro CLI)
+RUN curl -fsSL https://deb.nodesource.com/setup_22.x | bash - \
+    && apt-get install -y nodejs \
+    && rm -rf /var/lib/apt/lists/*
+
+# Install elan (Lean version manager) and the toolchain specified in lean-toolchain
+RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y --default-toolchain none
+ENV PATH="/root/.elan/bin:${PATH}"
+
+# Install cvc5 (required by Strata tests)
+RUN ARCH=$(uname -m) \
+    && if [ "$ARCH" = "x86_64" ]; then ARCH_NAME="x86_64"; \
+       elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then ARCH_NAME="arm64"; \
+       else echo "Unsupported architecture: $ARCH" && exit 1; fi \
+    && wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip \
+    && unzip -q cvc5-Linux-${ARCH_NAME}-static.zip \
+    && mv cvc5-Linux-${ARCH_NAME}-static/bin/cvc5 /usr/local/bin/ \
+    && rm -rf cvc5-Linux-${ARCH_NAME}-static*
+
+# Install z3 (required by Strata tests)
+RUN ARCH=$(uname -m) \
+    && if [ "$ARCH" = "x86_64" ]; then \
+         wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip \
+         && unzip -q z3-4.15.2-x64-glibc-2.39.zip \
+         && mv z3-4.15.2-x64-glibc-2.39/bin/z3 /usr/local/bin/ \
+         && rm -rf z3-4.15.2-x64-glibc-2.39*; \
+       elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then \
+         wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip \
+         && unzip -q z3-4.15.2-arm64-glibc-2.34.zip \
+         && mv z3-4.15.2-arm64-glibc-2.34/bin/z3 /usr/local/bin/ \
+         && rm -rf z3-4.15.2-arm64-glibc-2.34*; \
+       else echo "Unsupported architecture: $ARCH" && exit 1; fi
+
+# Install Claude Code CLI
+RUN npm install -g @anthropic-ai/claude-code
+
+# Install Kiro CLI
+RUN npm install -g kiro
+
+# Install uv (needed for lean-lsp-mcp via uvx)
+RUN pipx install uv
+ENV PATH="/root/.local/bin:${PATH}"
+
+WORKDIR /workspaces/Strata
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
new file mode 100644
index 0000000000..057f6c4340
--- /dev/null
+++ b/.devcontainer/devcontainer.json
@@ -0,0 +1,17 @@
+{
+  "name": "Strata",
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
+  "features": {
+    "ghcr.io/devcontainers/features/github-cli:1": {}
+  },
+  "postCreateCommand": ".devcontainer/postCreate.sh",
+  "customizations": {
+    "vscode": {
+      "extensions": [
+        "leanprover.lean4"
+      ]
+    }
+  }
+}
diff --git a/.devcontainer/postCreate.sh b/.devcontainer/postCreate.sh
new file mode 100755
index 0000000000..eb770d1d18
--- /dev/null
+++ b/.devcontainer/postCreate.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+set -euo pipefail
+
+# Install the Lean toolchain specified in lean-toolchain
+elan install "$(cat lean-toolchain)"
+
+# Build and test to populate the Lake cache
+lake build
+lake test -- --exclude Languages.Python
diff --git a/.kiro/settings/mcp.json b/.kiro/settings/mcp.json
index 29a35b076b..fedfc81326 100644
--- a/.kiro/settings/mcp.json
+++ b/.kiro/settings/mcp.json
@@ -27,6 +27,14 @@
         "lean_local_search",
         "lean_verify"
       ]
+    },
+    "github": {
+      "command": "npx",
+      "args": [
+        "-y",
+        "@modelcontextprotocol/server-github"
+      ],
+      "disabled": false
     }
   }
-}
\ No newline at end of file
+}