feat: add Nix flake for reproducible builds

.envrc

@@ -0,0 +1 @@
+use flake

.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

.gitignore

@@ -1,3 +1,7 @@
 .venv/
 .lake/
-build.log
+build.log
+result
+result-*
+.direnv/
+WIP.md

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

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];
+        };
+      };
+    };
+}

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