diff --git a/.github/workflows/amd64-linux-main-proof.yml b/.github/workflows/amd64-linux-main-proof.yml
index 2c61b8f4..1a423860 100644
--- a/.github/workflows/amd64-linux-main-proof.yml
+++ b/.github/workflows/amd64-linux-main-proof.yml
@@ -17,14 +17,21 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
-      - name: extract and check
-        run: JASMIN=$(which_jasminc) EASYCRYPT=$(which_easycrypt) ECARGS=$(which_eclib) make -j$JOBS -C proof/ CI=1 default
+      - uses: DeterminateSystems/magic-nix-cache-action@v4
 
-      - name: dist
-        run: ./scripts/ci/releaser/jdist-proof
+      - name: extract and check
+        uses: workflow/nix-shell-action@v3.3.0
+        with:
+          flakes: .
+          flakes-from-devshell: true
+          script: |
+            # extract and check
+            make -j$JOBS -C proof/ CI=1 default
+            # dist
+            ./scripts/ci/releaser/jdist-proof
 
       - name: print logs
-        run: JASMIN=$(which_jasminc) EASYCRYPT=$(which_easycrypt) ECARGS=$(which_eclib) make         -C proof/ CI=1 reporter
+        run: make         -C proof/ CI=1 reporter
 
       - name: return error if there are any errors
         run: make         -C proof/ CI=1 err
diff --git a/.github/workflows/amd64-linux-main.yml b/.github/workflows/amd64-linux-main.yml
index 6a1347d4..e16bcb7f 100644
--- a/.github/workflows/amd64-linux-main.yml
+++ b/.github/workflows/amd64-linux-main.yml
@@ -17,10 +17,17 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
+      - uses: DeterminateSystems/magic-nix-cache-action@v4
+
       - name: compile
-        run: JASMIN=$(which_jasminc) make -j$JOBS -C src/ CI=1 default
+        uses: workflow/nix-shell-action@v3.3.0
+        with:
+          flakes: .
+          flakes-from-devshell: true
+          script: make -j$JOBS -C src/ CI=1 default
+
       - name: print logs
-        run: JASMIN=$(which_jasminc) make -C src/ CI=1 reporter
+        run: make -C src/ CI=1 reporter
       - name: return error if there are any errors
         run: make -C src/ CI=1 err
 
@@ -40,10 +47,17 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
+      - uses: DeterminateSystems/magic-nix-cache-action@v4
+
       - name: compile and run
-        run: JASMIN=$(which_jasminc) make -j$JOBS -C test/ CI=1 default
+        uses: workflow/nix-shell-action@v3.3.0
+        with:
+          flakes: .
+          flakes-from-devshell: true
+          script: make -j$JOBS -C test/ CI=1 default
+
       - name: print logs
-        run: JASMIN=$(which_jasminc) make -C test/ CI=1 reporter
+        run: make -C test/ CI=1 reporter
       - name: return error if there are any errors
         run: make -C test/ CI=1 err
 
@@ -63,14 +77,20 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
+      - uses: DeterminateSystems/magic-nix-cache-action@v4
+
       - name: compile
-        run: JASMIN=$(which_jasminc) make -j$JOBS -C src/   CI=1 default
+        uses: workflow/nix-shell-action@v3.3.0
+        with:
+          flakes: .
+          flakes-from-devshell: true
+          script: make -j$JOBS -C src/   CI=1 default
 
       - name: run
-        run: JASMIN=$(which_jasminc) make -j$JOBS -C bench/ CI=1 DEFINE='-DTIMINGS=10' run
+        run: make -j$JOBS -C bench/ CI=1 DEFINE='-DTIMINGS=10' run
 
       - name: print logs
-        run: JASMIN=$(which_jasminc) make -C bench/ CI=1 reporter
+        run: make -C bench/ CI=1 reporter
 
       - name: return error if there are any errors
         run: make -C bench/ CI=1 err
@@ -91,14 +111,20 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
+      - uses: DeterminateSystems/magic-nix-cache-action@v4
+
       - name: compile
-        run: JASMIN=$(which_jasminc) make -j$JOBS -C src/   CI=1 default
+        uses: workflow/nix-shell-action@v3.3.0
+        with:
+          flakes: .
+          flakes-from-devshell: true
+          script: make -j$JOBS -C src/   CI=1 default
 
       - name: run
-        run: JASMIN=$(which_jasminc) make -j$JOBS -C bench/ CI=1 run DEFINE='-DTIMINGS=10 -DRUNS=2 -DST_ON' RANDINC='../test/common/' RANDLIB='../test/common/notrandombytes.c';
+        run: make -j$JOBS -C bench/ CI=1 run DEFINE='-DTIMINGS=10 -DRUNS=2 -DST_ON' RANDINC='../test/common/' RANDLIB='../test/common/notrandombytes.c';
 
       - name: print logs
-        run: JASMIN=$(which_jasminc) make -C bench/ CI=1 reporter
+        run: make -C bench/ CI=1 reporter
 
       - name: return error if there are any errors
         run: make -C bench/ CI=1 err
@@ -119,12 +145,22 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
+      - uses: DeterminateSystems/magic-nix-cache-action@v4
+
       - name: extract and check
-        run: JASMIN=$(which_jasminc) EASYCRYPT=$(which_easycrypt) ECARGS=$(which_eclib) make -j$JOBS -C proof/ CI=1 check-extracted
-      - name: dist
-        run: ./scripts/ci/releaser/jdist-proof
+        uses: workflow/nix-shell-action@v3.3.0
+        with:
+          flakes: .
+          flakes-from-devshell: true
+          script: |
+            # extract and check
+            make -j$JOBS -C proof/ CI=1 check-extracted
+            # dist
+            ./scripts/ci/releaser/jdist-proof
+
       - name: print logs
-        run: JASMIN=$(which_jasminc) EASYCRYPT=$(which_easycrypt) ECARGS=$(which_eclib) make -C proof/ CI=1 reporter
+        run: make -C proof/ CI=1 reporter
+
       - name: return error if there are any errors
         run: make -C proof/ CI=1 err
 
@@ -151,14 +187,20 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
-      - name: compile amd64
-        run: JASMIN=$(which_jasminc) make -j$JOBS -C src/ CI=1 default
+      - uses: DeterminateSystems/magic-nix-cache-action@v4
 
       - name: dist amd64
-        run: JASMIN=$(which_jasminc) ./scripts/ci/releaser/jdist-src-v1 amd64
-
-      - name: check dist amd64
-        run: JASMIN=$(which_jasminc) ./scripts/ci/releaser/jdist-src-test-v1 amd64
+        uses: workflow/nix-shell-action@v3.3.0
+        with:
+          flakes: .
+          flakes-from-devshell: true
+          script: |
+            # compile amd64
+            make -j$JOBS -C src/ CI=1 default
+            # dist amd64
+            ./scripts/ci/releaser/jdist-src-v1 amd64
+            # check dist amd64
+            ./scripts/ci/releaser/jdist-src-test-v1 amd64
 
       - name: libjade-dist-src-amd64.tar.gz - contains assembly, Jasmin, and how-to-use code
         if: always()
diff --git a/.gitignore b/.gitignore
index 76f14337..b2169480 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 .ci
 *.tar.gz
 libjade-*
-.vscode
\ No newline at end of file
+.vscode
+result
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 00000000..53c68883
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,315 @@
+{
+  "nodes": {
+    "easycrypt": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": [
+          "easycrypt",
+          "opam-nix",
+          "nixpkgs"
+        ],
+        "opam-nix": "opam-nix",
+        "prover_cvc4_1_8": "prover_cvc4_1_8",
+        "prover_cvc5_1_0_5": "prover_cvc5_1_0_5",
+        "prover_z3_4_12_6": "prover_z3_4_12_6",
+        "stable": "stable"
+      },
+      "locked": {
+        "lastModified": 1712580297,
+        "narHash": "sha256-3zpAbtDN7eFKjzCUExdl6lpidzprw5wzNEduQ1zGWHs=",
+        "owner": "EasyCrypt",
+        "repo": "easycrypt",
+        "rev": "4201fddc14b81d2a69a33f034c9c7db4dfd58d0e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "EasyCrypt",
+        "repo": "easycrypt",
+        "rev": "4201fddc14b81d2a69a33f034c9c7db4dfd58d0e",
+        "type": "github"
+      }
+    },
+    "flake-compat": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1627913399,
+        "narHash": "sha256-hY8g6H2KFL8ownSiFeMOjwPC8P0ueXpCVEbxgda3pko=",
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "rev": "12c64ca55c1014cdc1b16ed5a804aa8576601ff2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1709126324,
+        "narHash": "sha256-q6EQdSeUZOG26WelxqkmR7kArjgWCdw5sfJVHPH/7j8=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "d465f4819400de7c8d874d50b982301f28a84605",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "flake-utils_2": {
+      "locked": {
+        "lastModified": 1638122382,
+        "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "74f7e4319258e287b0f9cb95426c9853b282730b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "jasmin": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1712566927,
+        "narHash": "sha256-sRegD+ecNeKUf0STO/2WRST2+CoEqdBdCAd478/zI8o=",
+        "owner": "jasmin-lang",
+        "repo": "jasmin",
+        "rev": "e84c0c59b4f4e005f2be4de5fdfbcaf1e3e2f975",
+        "type": "github"
+      },
+      "original": {
+        "owner": "jasmin-lang",
+        "repo": "jasmin",
+        "rev": "e84c0c59b4f4e005f2be4de5fdfbcaf1e3e2f975",
+        "type": "github"
+      }
+    },
+    "mirage-opam-overlays": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1661959605,
+        "narHash": "sha256-CPTuhYML3F4J58flfp3ZbMNhkRkVFKmBEYBZY5tnQwA=",
+        "owner": "dune-universe",
+        "repo": "mirage-opam-overlays",
+        "rev": "05f1c1823d891ce4d8adab91f5db3ac51d86dc0b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "dune-universe",
+        "repo": "mirage-opam-overlays",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1682362401,
+        "narHash": "sha256-/UMUHtF2CyYNl4b60Z2y4wwTTdIWGKhj9H301EDcT9M=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "884ac294018409e0d1adc0cae185439a44bd6b0b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1713362983,
+        "narHash": "sha256-glRKaESbOIEQRU5aZZu/T18rNaqNnBKDVag1EsfylpQ=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "8bc628c7d96aa5cf767bad443091f39aed0cbad0",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "ref": "release-23.11",
+        "type": "indirect"
+      }
+    },
+    "opam-nix": {
+      "inputs": {
+        "flake-compat": "flake-compat",
+        "flake-utils": "flake-utils_2",
+        "mirage-opam-overlays": "mirage-opam-overlays",
+        "nixpkgs": "nixpkgs",
+        "opam-overlays": "opam-overlays",
+        "opam-repository": "opam-repository",
+        "opam2json": "opam2json"
+      },
+      "locked": {
+        "lastModified": 1706878465,
+        "narHash": "sha256-0k0KSkU7epRQshZZKsOpyE79lnwn/0q2VagzDhIeZpE=",
+        "owner": "tweag",
+        "repo": "opam-nix",
+        "rev": "9f03f7e0664c369f25e614d3f3be74ea78b647fa",
+        "type": "github"
+      },
+      "original": {
+        "owner": "tweag",
+        "repo": "opam-nix",
+        "type": "github"
+      }
+    },
+    "opam-overlays": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1654162756,
+        "narHash": "sha256-RV68fUK+O3zTx61iiHIoS0LvIk0E4voMp+0SwRg6G6c=",
+        "owner": "dune-universe",
+        "repo": "opam-overlays",
+        "rev": "c8f6ef0fc5272f254df4a971a47de7848cc1c8a4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "dune-universe",
+        "repo": "opam-overlays",
+        "type": "github"
+      }
+    },
+    "opam-repository": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1705008664,
+        "narHash": "sha256-TTjTal49QK2U0yVOmw6rJhTGYM7tnj3Kv9DiEEiLt7E=",
+        "owner": "ocaml",
+        "repo": "opam-repository",
+        "rev": "fa77046c6497f8ca32926acdb7eb1e61777d4c17",
+        "type": "github"
+      },
+      "original": {
+        "owner": "ocaml",
+        "repo": "opam-repository",
+        "type": "github"
+      }
+    },
+    "opam2json": {
+      "inputs": {
+        "nixpkgs": [
+          "easycrypt",
+          "opam-nix",
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1671540003,
+        "narHash": "sha256-5pXfbUfpVABtKbii6aaI2EdAZTjHJ2QntEf0QD2O5AM=",
+        "owner": "tweag",
+        "repo": "opam2json",
+        "rev": "819d291ea95e271b0e6027679de6abb4d4f7f680",
+        "type": "github"
+      },
+      "original": {
+        "owner": "tweag",
+        "repo": "opam2json",
+        "type": "github"
+      }
+    },
+    "prover_cvc4_1_8": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1592585967,
+        "narHash": "sha256-V6KShPLW6kFBJaNgqy98rjOxULmf5c8AmDwo9fclGuY=",
+        "owner": "CVC4",
+        "repo": "CVC4-archived",
+        "rev": "5247901077efbc7b9016ba35fded7a6ab459a379",
+        "type": "github"
+      },
+      "original": {
+        "owner": "CVC4",
+        "ref": "1.8",
+        "repo": "CVC4-archived",
+        "type": "github"
+      }
+    },
+    "prover_cvc5_1_0_5": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1678724158,
+        "narHash": "sha256-l+L59QLLrAEVkAZjhxICJpa+j+jr1k/7B61JlapXGRI=",
+        "owner": "cvc5",
+        "repo": "cvc5",
+        "rev": "4cb2ab9eb36f64295272a50f61dd1c62903aca4b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "cvc5",
+        "ref": "cvc5-1.0.5",
+        "repo": "cvc5",
+        "type": "github"
+      }
+    },
+    "prover_z3_4_12_6": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1708814107,
+        "narHash": "sha256-X4wfPWVSswENV0zXJp/5u9SQwGJWocLKJ/CNv57Bt+E=",
+        "owner": "z3prover",
+        "repo": "z3",
+        "rev": "fa2c0e027894a8d55d2b841e27cbeecc99692a3f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "z3prover",
+        "ref": "z3-4.12.6",
+        "repo": "z3",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "easycrypt": "easycrypt",
+        "jasmin": "jasmin",
+        "nixpkgs": "nixpkgs_2"
+      }
+    },
+    "stable": {
+      "locked": {
+        "lastModified": 1701282334,
+        "narHash": "sha256-MxCVrXY6v4QmfTwIysjjaX0XUhqBbxTWWB4HXtDYsdk=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "057f9aecfb71c4437d2b27d3323df7f93c010b7e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "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 00000000..dc53bff1
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,65 @@
+{
+  description = "Libjade";
+
+  inputs = {
+    nixpkgs.url = "nixpkgs/release-23.11";
+    easycrypt.url = "github:EasyCrypt/easycrypt/4201fddc14b81d2a69a33f034c9c7db4dfd58d0e";
+    jasmin = {
+      url = "github:jasmin-lang/jasmin/e84c0c59b4f4e005f2be4de5fdfbcaf1e3e2f975";
+      flake = false;
+    };
+  };
+
+  outputs = { self, nixpkgs, easycrypt, jasmin, ... }:
+    let
+      system = "x86_64-linux";
+      pkgs = nixpkgs.legacyPackages.${system};
+      jasminc = pkgs.callPackage "${jasmin}/default.nix" { inherit pkgs; };
+      ec = easycrypt.packages.${system}.default;
+    in
+    {
+      packages.${system}.default = pkgs.stdenv.mkDerivation {
+        name = "libjade";
+        src = ./src;
+
+        nativeBuildInputs = with pkgs; [
+          jasminc
+          clang
+          gnumake
+        ];
+
+        buildPhase = ''
+          make FAIL_ON_ERROR=1 -j$(nproc)
+        '';
+
+        installPhase = ''
+          mkdir -p $out/lib
+          mkdir -p $out/include
+          cp libjade.a $out/lib/
+          cp libjade.h $out/include/
+        '';
+
+      };
+
+      devShells.${system}.default = pkgs.mkShell {
+        name = "libjade-ci";
+        src = self.packages.${system}.default.src;
+
+        packages = self.packages.${system}.default.nativeBuildInputs ++
+          [
+            ec
+            pkgs.valgrind
+            pkgs.cvc4
+            pkgs.cvc5
+            pkgs.z3
+          ];
+
+        EASYCRYPT = "${ec}/bin/easycrypt";
+        ECARGS = "-I Jasmin:${jasmin}/eclib";
+
+        shellHook = ''
+          easycrypt why3config
+        '';
+      };
+    };
+}
diff --git a/src/Makefile b/src/Makefile
index 14f11b7c..1001829f 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -29,6 +29,8 @@ ASM     := $(shell find $(SRC) -name '*.s')
 API     := $(addsuffix include/api.h, $(dir $(ASM)))
 OBJ     := $(ASM:%.s=%.o)
 
+FAIL_ON_ERROR ?= 0
+
 # --------------------------------------------------------------------
 ifeq ($(CI),1)
 .PHONY: backward_compatibility
@@ -56,7 +58,7 @@ __libjade: $(OBJ)
 	echo "" | cat - $(API) > libjade.h
 
 $(JAZZ):
-	$(MAKE) -C $@ || true
+	$(MAKE) -C $@ || !(($(FAIL_ON_ERROR)))
 
 # --------------------------------------------------------------------