diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/.github/workflows/ci-nix.yaml b/.github/workflows/ci-nix.yaml
new file mode 100644
index 0000000..5996ba5
--- /dev/null
+++ b/.github/workflows/ci-nix.yaml
@@ -0,0 +1,24 @@
+name: ci-nix
+
+permissions:
+  contents: read
+
+on:
+  workflow_dispatch:
+
+concurrency:
+  group: nix-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v30
+
+      - name: Run flake checks
+        run: nix flake check -L
diff --git a/.gitignore b/.gitignore
index e781e70..7a089cd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,7 @@
 .venv/
 .lake/
-build.log
\ No newline at end of file
+build.log
+result
+result-*
+.direnv/
+WIP.md
\ No newline at end of file
diff --git a/README.md b/README.md
index 9940620..a537f48 100644
--- a/README.md
+++ b/README.md
@@ -36,6 +36,7 @@ Blaster provides an SMT backend for Z3 proofs. Blaster works by first aggressive
     - [Function propagation](#function-propagation)
   - [Second-step: SMT Translation](#second-step-smt-translation)
   - [Final step: SMT Solver Interaction](#final-step-smt-solver-interaction)
+- [Nix (NixOS / direnv)](#nix-nixos--direnv)
 - [Installing the Z3 Solver](#installing-the-z3-solver)
 - [Contributing](#contributing)
   - [Ways to Contribute](#ways-to-contribute)
@@ -526,6 +527,39 @@ Once an expression has been translated, Blaster interacts with an external SMT s
 
 ---
 
+## Nix (NixOS / direnv)
+
+A Nix flake is provided for reproducible builds and development. It pins the exact Lean and Z3 versions required by Blaster.
+
+### Development shell
+
+```bash
+nix develop    # or use direnv with the included .envrc
+```
+
+This gives you Lean 4.24.0, Z3 4.15.2, Lake, and elan — everything needed for `lake build` and VS Code with the [Lean 4 extension](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4).
+
+### Building
+
+```bash
+nix build              # Blaster library
+nix build .#z3check    # z3check executable (Z3 in PATH)
+```
+
+### Checks
+
+```bash
+nix flake check        # builds library, z3check, and the full test suite
+```
+
+The test suite compiles every module in `Tests/` with Z3 4.15.2 injected into the build sandbox.
+
+### CI
+
+The `ci-nix` workflow can be triggered manually from the Actions tab. It runs `nix flake check` on `ubuntu-latest`.
+
+---
+
 ## Installing the Z3 Solver
 
 Blaster requires Z3 version 4.15.2.  To install that, you need to
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..be8af44
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,117 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1772408722,
+        "narHash": "sha256-rHuJtdcOjK7rAHpHphUb1iCvgkU3GpfvicLMwwnfMT0=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "f20dc5d9b8027381c474144ecabc9034d6a839a3",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "flake-parts_2": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib_2"
+      },
+      "locked": {
+        "lastModified": 1765835352,
+        "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "a34fae9c08a15ad73f295041fec82323541400a9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "lean4-nix": {
+      "inputs": {
+        "flake-parts": "flake-parts_2",
+        "nixpkgs": "nixpkgs"
+      },
+      "locked": {
+        "lastModified": 1771875971,
+        "narHash": "sha256-D3PN4o8RtyHEjlAtsLa6M9xRjIwtMUk4pIkfsNSMAvQ=",
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
+        "rev": "faebfa2e0d7093fea3ffaa493b316bf3449c1dbf",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1765779637,
+        "narHash": "sha256-KJ2wa/BLSrTqDjbfyNx70ov/HdgNBCBBSQP3BIzKnv4=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "1306659b587dc277866c7b69eb97e5f07864d8c4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "lastModified": 1772328832,
+        "narHash": "sha256-e+/T/pmEkLP6BHhYjx6GmwP5ivonQQn0bJdH9YrRB+Q=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "c185c7a5e5dd8f9add5b2f8ebeff00888b070742",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib_2": {
+      "locked": {
+        "lastModified": 1765674936,
+        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "lean4-nix": "lean4-nix",
+        "nixpkgs": [
+          "lean4-nix",
+          "nixpkgs"
+        ]
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..b6acbc5
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,110 @@
+{
+  description = "Lean Blaster — SMT-based tactic for Lean 4";
+
+  inputs = {
+    nixpkgs.follows = "lean4-nix/nixpkgs";
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    lean4-nix.url = "github:lenianiva/lean4-nix";
+  };
+
+  outputs = inputs @ {
+    nixpkgs,
+    flake-parts,
+    lean4-nix,
+    ...
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      systems = [
+        "x86_64-linux"
+        "aarch64-darwin"
+      ];
+
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: let
+        leanPkgs = pkgs.lean;
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type: let
+            baseName = builtins.baseNameOf (toString path);
+          in
+            pkgs.lib.cleanSourceFilter path type
+            && baseName != ".lake"
+            && baseName != ".direnv"
+            && !(pkgs.lib.hasPrefix "result" baseName);
+        };
+        inherit (pkgs) makeWrapper;
+        blaster = leanPkgs.buildLeanPackage {
+          name = "Blaster";
+          roots = ["Blaster"];
+          inherit src;
+          leancFlags = ["-O3"];
+        };
+        z3check = leanPkgs.buildLeanPackage {
+          name = "Z3Check";
+          roots = ["Z3Check"];
+          inherit src;
+        };
+        z3checkWrapped = pkgs.runCommand "z3check" {nativeBuildInputs = [makeWrapper];} ''
+          mkdir -p $out/bin
+          cp ${z3check.executable}/bin/* $out/bin/
+          wrapProgram $out/bin/z3check --prefix PATH : ${pkgs.lib.makeBinPath [pkgs.z3]}
+        '';
+        tests = leanPkgs.buildLeanPackage {
+          name = "Tests";
+          roots = ["Tests"];
+          deps = [blaster];
+          inherit src;
+          overrideBuildModAttrs = _final: prev: {
+            buildInputs = (prev.buildInputs or []) ++ [pkgs.z3];
+          };
+        };
+      in {
+        _module.args.pkgs = import nixpkgs {
+          inherit system;
+          overlays = [
+            (lean4-nix.readToolchainFile ./lean-toolchain)
+            (_final: prev: {
+              z3 = prev.z3.overrideAttrs {
+                version = "4.15.2";
+                src = prev.fetchFromGitHub {
+                  owner = "Z3Prover";
+                  repo = "z3";
+                  rev = "z3-4.15.2";
+                  hash = "sha256-hUGZdr0VPxZ0mEUpcck1AC0MpyZMjiMw/kK8WX7t0xU=";
+                };
+              };
+            })
+          ];
+        };
+
+        packages = {
+          default = blaster.modRoot;
+          z3check = z3checkWrapped;
+        };
+
+        checks = {
+          blaster = blaster.modRoot;
+          z3check = z3checkWrapped;
+          tests = tests.modRoot;
+          smoke-test = pkgs.runCommand "blaster-smoke-test" {
+            buildInputs = [leanPkgs.lean-all pkgs.z3];
+            LEAN_PATH = "${blaster.modRoot}";
+          } ''
+            lean ${src}/tests/nix/TestBlaster.lean
+            touch $out
+          '';
+        };
+
+        legacyPackages = {
+          inherit blaster tests z3check;
+        };
+
+        devShells.default = pkgs.mkShell {
+          packages = [leanPkgs.lean-all pkgs.z3 pkgs.elan];
+        };
+      };
+    };
+}
diff --git a/tests/nix/TestBlaster.lean b/tests/nix/TestBlaster.lean
new file mode 100644
index 0000000..4856152
--- /dev/null
+++ b/tests/nix/TestBlaster.lean
@@ -0,0 +1,10 @@
+import Blaster
+
+-- Propositional logic
+example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by blaster
+
+-- Linear arithmetic
+example (x y : Nat) (h1 : x + y > 0) (h2 : y > 0) : x + y > 0 := by blaster
+
+-- De Morgan
+example (p q : Prop) (h : ¬(p ∨ q)) : ¬p ∧ ¬q := by blaster