diff --git a/.envrc b/.envrc
new file mode 100644
index 000000000..3550a30f2
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/.github/workflows/nix.yaml b/.github/workflows/nix.yaml
new file mode 100644
index 000000000..8338fb08b
--- /dev/null
+++ b/.github/workflows/nix.yaml
@@ -0,0 +1,17 @@
+# This workflow tests the Nix build of pulse. We run it only for PRs (not
+# on every push) and we use Github hosted runners.
+
+name: Nix Build
+
+on:
+  pull_request:
+
+jobs:
+  nix-build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: DeterminateSystems/nix-installer-action@main
+    - uses: DeterminateSystems/magic-nix-cache-action@main
+    - name: Build
+      run: nix build -L
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 000000000..3a0045f35
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,129 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1743550720,
+        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1692799911,
+        "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44",
+        "type": "github"
+      },
+      "original": {
+        "id": "flake-utils",
+        "type": "indirect"
+      }
+    },
+    "fstar": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      },
+      "locked": {
+        "lastModified": 1742959035,
+        "narHash": "sha256-PhjfThXF6fJlFHtNEURG4igCnM6VegWODypmRvnZPdA=",
+        "owner": "FStarLang",
+        "repo": "FStar",
+        "rev": "71d8221589d4d438af3706d89cb653cf53e18aab",
+        "type": "github"
+      },
+      "original": {
+        "owner": "FStarLang",
+        "ref": "v2025.03.25",
+        "repo": "FStar",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1743588408,
+        "narHash": "sha256-WRZyK13yucGjwNBMOGjU8ljRJ8FYFv8MBru/bXqZUn0=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "88efe689298b1863db0310c0a22b3ebb4d04fbc3",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "ref": "nixos-unstable",
+        "type": "indirect"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "lastModified": 1743296961,
+        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1745930157,
+        "narHash": "sha256-y3h3NLnzRSiUkYpnfvnS669zWZLoqqI6NprtLQ+5dck=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "46e634be05ce9dc6d4db8e664515ba10b78151ae",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "fstar": "fstar",
+        "nixpkgs": "nixpkgs_2"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 000000000..4f657c547
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,123 @@
+{
+  inputs = {
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    fstar.url = "github:FStarLang/FStar/v2025.03.25";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+  };
+
+  outputs = { ... }@inputs:
+
+    inputs.flake-parts.lib.mkFlake { inherit inputs; } {
+
+      systems = inputs.nixpkgs.lib.systems.flakeExposed;
+      imports = [ ];
+
+      perSystem = { pkgs, config, system, ... }: {
+
+        packages.pulse = pkgs.stdenv.mkDerivation rec {
+
+          pname = "pulse";
+          version = "9a03472d2c366bde5f7b0497bf3356dd445ce207";
+          src = pkgs.fetchFromGitHub {
+            owner = "FStarLang";
+            repo = pname;
+            rev = "${version}";
+            hash = "sha256-YgWxnX+gCVYx+CCIuprDYKewyEaSekqAilB96eyq+fk=";
+          };
+
+          inherit (pkgs.fstar) nativeBuildInputs;
+          buildInputs = pkgs.fstar.buildInputs ++ [
+            pkgs.fstar
+            pkgs.which
+          ];
+          PATH = "${pkgs.fstar}/bin:$PATH";
+
+          enableParallelBuilding = true;
+
+          installPhase = ''
+            PREFIX=$out make install
+          '';
+
+        };
+
+        packages.pulse-exe = pkgs.writeShellScriptBin "pulse.exe" ''
+          exec ${pkgs.fstar}/bin/fstar.exe "$1" \
+            --include ${config.packages.pulse}/lib/pulse \
+            --include ${config.packages.pulse}/lib/pulse/checker \
+            --include ${config.packages.pulse}/lib/pulse/extraction \
+            --include ${config.packages.pulse}/lib/pulse/lib \
+            --include ${config.packages.pulse}/lib/pulse/ml \
+            --include ${config.packages.pulse}/lib/pulse/syntax_extension \
+            --load_cmxs pulse \
+            "$@"
+        '';
+
+        packages.rustast-bindings = pkgs.rustPlatform.buildRustPackage rec {
+          inherit (config.packages.pulse) version src;
+          inherit (pkgs.fstar) nativeBuildInputs;
+          pname = "rustast-bindings";
+          sourceRoot = "${src.name}/pulse2rust/src/ocaml";
+          cargoLock = {
+            lockFile = ./pulse2rust/src/ocaml/Cargo.lock;
+          };
+          postPatch = ''
+            ln -s ${./pulse2rust/src/ocaml/Cargo.lock} Cargo.lock
+          '';
+        };
+
+        packages.extract = pkgs.stdenv.mkDerivation {
+          pname = "extract";
+          inherit (config.packages.pulse) version;
+          src = pkgs.fetchFromGitHub {
+            owner = "FStarLang";
+            repo = "pulse";
+            rev = "42842b823c45f83376b65bc10ffa803ad6f21dc4";
+            hash = "sha256-CRlrfiDXoSn9s0tiU4dunsUsUu00jb8U9/QApfu+Qtw=";
+          };
+          sourceRoot = "source/pulse2rust/src";
+          buildInputs = [
+            pkgs.fstar
+            pkgs.which
+          ];
+          PATH = "${pkgs.fstar}/bin:$PATH";
+
+          installPhase = ''
+            mkdir -p $out/ocaml/generated
+            cp -r ocaml/generated $out/ocaml
+          '';
+        };
+
+        packages.pulse2rust = inputs.fstar.inputs.nixpkgs.legacyPackages.${system}.ocaml-ng.ocamlPackages_4_14.buildDunePackage rec {
+          inherit (config.packages.pulse) version src;
+          pname = "main";
+          sourceRoot = "${src.name}/pulse2rust/src/ocaml";
+
+          nativeBuildInputs = pkgs.fstar.nativeBuildInputs ++ [ pkgs.fstar ];
+          buildInputs = pkgs.fstar.buildInputs ++ [ pkgs.fstar ];
+
+          buildPhase = ''
+            eval $(${pkgs.fstar}/bin/fstar.exe --ocamlenv)
+            mkdir -p $out/bin
+            dune build main.exe --build-dir=$out/bin
+          '';
+
+          postPatch = ''
+            ln -s ${./pulse2rust/src/dune-project} dune-project
+            ln -s ${config.packages.rustast-bindings}/lib/librustast_bindings.a librustast_bindings.a
+            mkdir -p ocaml/generated
+            cp -r ${config.packages.extract}/ocaml/generated ocaml
+          '';
+
+          # overwrites the default dune installPhase
+          installPhase = '''';
+
+          meta.mainProgram = "default/ocaml/main.exe";
+        };
+
+        packages.fstar = pkgs.fstar;
+
+        packages.default = config.packages.pulse;
+
+      };
+    };
+}
\ No newline at end of file
diff --git a/pulse2rust/src/ocaml/Cargo.lock b/pulse2rust/src/ocaml/Cargo.lock
new file mode 100644
index 000000000..c76e9cb84
--- /dev/null
+++ b/pulse2rust/src/ocaml/Cargo.lock
@@ -0,0 +1,115 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "cc"
+version = "1.2.16"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "be714c154be609ec7f5dad223a33bf1482fff90472de28f7362806e6d4832b8c"
+dependencies = [
+ "shlex",
+]
+
+[[package]]
+name = "cty"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b365fabc795046672053e29c954733ec3b05e4be654ab130fe8f1f94d7051f35"
+
+[[package]]
+name = "ocaml-boxroot-sys"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5186393bfbee4ce2bc5bbb82beafb77e85c1d0a557e3cfc8c8a0d63d7845fed5"
+dependencies = [
+ "cc",
+]
+
+[[package]]
+name = "ocaml-interop"
+version = "0.9.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ce6dfec8cfe7907ee7c62a853f849861f05747f3514126bfdb7c0c842513a9e"
+dependencies = [
+ "ocaml-boxroot-sys",
+ "ocaml-sys",
+ "static_assertions",
+]
+
+[[package]]
+name = "ocaml-sys"
+version = "0.22.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "73ec6ca7d41458442627435afb8f4671e83fd642e8a560171d671a1f679aa3cf"
+dependencies = [
+ "cty",
+]
+
+[[package]]
+name = "prettyplease"
+version = "0.2.29"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6924ced06e1f7dfe3fa48d57b9f74f55d8915f5036121bef647ef4b204895fac"
+dependencies = [
+ "proc-macro2",
+ "syn",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.94"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a31971752e70b8b2686d7e46ec17fb38dad4051d94024c88df49b667caea9c84"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.39"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c1f1914ce909e1658d9907913b4b91947430c7d9be598b15a1912935b8c04801"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "rustast_bindings"
+version = "0.1.0"
+dependencies = [
+ "ocaml-interop",
+ "prettyplease",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "shlex"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
+
+[[package]]
+name = "static_assertions"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f"
+
+[[package]]
+name = "syn"
+version = "2.0.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e02e925281e18ffd9d640e234264753c43edc62d64b2d4cf898f1bc5e75f3fc2"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "00e2473a93778eb0bad35909dff6a10d28e63f792f16ed15e404fca9d5eeedbe"