From 0290bfca3820e6183f2090cfda44580a34be9264 Mon Sep 17 00:00:00 2001
From: Raoul <raoul.schaffranek@runtimeverification.com>
Date: Tue, 13 Oct 2026 12:24:16 +0000
Subject: [PATCH 1/4] Inlcude the k-semantics in nix build

---
 README.md                                     |   6 +-
 flake.nix                                     |   5 +-
 .../build-systems-overlay.nix                 |   0
 nix/kontrol-node-pyk/default.nix              |  59 +++++++++
 nix/kontrol-node/default.nix                  | 119 +++++++++++-------
 src/kontrol_node/__main__.py                  |   6 +-
 src/kontrol_node/rpc.py                       |  50 +++++++-
 7 files changed, 188 insertions(+), 57 deletions(-)
 rename nix/{kontrol-node => kontrol-node-pyk}/build-systems-overlay.nix (100%)
 create mode 100644 nix/kontrol-node-pyk/default.nix

diff --git a/README.md b/README.md
index 7c8358f1..eabff777 100644
--- a/README.md
+++ b/README.md
@@ -85,6 +85,9 @@ kontrol-node run --port 8545              # use the conventional Ethereum port
 kontrol-node run --host 0.0.0.0           # accept connections from outside localhost
 ```
 
+Once the node accepts requests it prints `Listening on http://<host>:<port>`; scripts can wait for
+that line before sending requests.
+
 Chain state lives in a fresh `io_dir*` directory under the working directory and is removed on exit,
 so **every run starts from genesis**. Requests are handled one at a time.
 
@@ -343,7 +346,8 @@ uv run kdist clean
 ```
 
 See `kdist --help` for all options. A Nix flake is also provided: `nix develop` gives a shell with K
-and every build dependency, `nix build` builds the package.
+and every build dependency, `nix build` builds the package — the same one `kup` installs, with the
+matching K and the compiled semantics bundled.
 
 To build and install the wheel:
 
diff --git a/flake.nix b/flake.nix
index bf80483d..97ee6ef6 100644
--- a/flake.nix
+++ b/flake.nix
@@ -55,10 +55,11 @@
         k = k-framework.packages.${system}.k;
       };
       kontrol-nodeOverlay = final: prev: {
-        kontrol-node = final.callPackage ./nix/kontrol-node {
+        kontrol-node-pyk = final.callPackage ./nix/kontrol-node-pyk {
           inherit pyproject-nix pyproject-build-systems uv2nix;
           python = final."python${pythonVer}";
         };
+        kontrol-node = final.callPackage ./nix/kontrol-node { };
       };
       pkgs = import nixpkgs {
         inherit system;
@@ -107,7 +108,7 @@
         '';
       };
       packages = rec {
-        inherit (pkgs) kontrol-node;
+        inherit (pkgs) kontrol-node kontrol-node-pyk;
         default = kontrol-node;
       };
     }) // {
diff --git a/nix/kontrol-node/build-systems-overlay.nix b/nix/kontrol-node-pyk/build-systems-overlay.nix
similarity index 100%
rename from nix/kontrol-node/build-systems-overlay.nix
rename to nix/kontrol-node-pyk/build-systems-overlay.nix
diff --git a/nix/kontrol-node-pyk/default.nix b/nix/kontrol-node-pyk/default.nix
new file mode 100644
index 00000000..a949dffc
--- /dev/null
+++ b/nix/kontrol-node-pyk/default.nix
@@ -0,0 +1,59 @@
+{
+  lib,
+  callPackage,
+  nix-gitignore,
+
+  pyproject-nix,
+  pyproject-build-systems,
+  uv2nix,
+
+  python
+}:
+let
+  pyproject-util = callPackage pyproject-nix.build.util {};
+  pyproject-packages = callPackage pyproject-nix.build.packages {
+    inherit python;
+  };
+
+  # load a uv workspace from a workspace root
+  workspace = uv2nix.lib.workspace.loadWorkspace {
+    workspaceRoot = lib.cleanSource (nix-gitignore.gitignoreSourcePure [
+        ../../.gitignore
+        ".github/"
+        "result*"
+        # do not include submodule directories that might be initilized empty or non-existent due to nix/git
+        # otherwise cachix build might not match the version that is requested by `kup`
+        # TODO: for new projects, add your submodule directories that are not required for nix builds here!
+        # e.g., `"/docs/external-computation"` with `external-computation` being a git submodule directory
+        # "/docs/external-computation"
+      ] ../..
+    );
+  };
+
+  # create overlay
+  lockFileOverlay = workspace.mkPyprojectOverlay {
+    # prefer "wheel" over "sdist" due to maintance overhead
+    # there is no bundled set of overlays for "sdist" in uv2nix, in contrast to poetry2nix
+    sourcePreference = "wheel";
+  };
+
+  buildSystemsOverlay = import ./build-systems-overlay.nix;
+
+  # construct package set
+  pythonSet = pyproject-packages.overrideScope (lib.composeManyExtensions [
+    # make build tools available by default as these are not necessarily specified in python lock files
+    pyproject-build-systems.overlays.default
+    # include all packages from the python lock file
+    lockFileOverlay
+    # add build system overrides to certain python packages
+    buildSystemsOverlay
+  ]);
+  # default dependancy group enables no optional dependencies and no dependency-groups
+  venv = pythonSet.mkVirtualEnv "kontrol-node-env" workspace.deps.default;
+in (pyproject-util.mkApplication {
+  inherit venv;
+  package = pythonSet.kontrol-node;
+}).overrideAttrs (old: {
+  # the application only exposes `kontrol-node`; the venv also provides `kdist` to build the semantics
+  passthru = (old.passthru or { }) // { inherit venv; };
+})
diff --git a/nix/kontrol-node/default.nix b/nix/kontrol-node/default.nix
index baabf6ca..caec1e3c 100644
--- a/nix/kontrol-node/default.nix
+++ b/nix/kontrol-node/default.nix
@@ -1,55 +1,78 @@
 {
   lib,
-  callPackage,
-  nix-gitignore,
+  stdenv,
+  makeWrapper,
 
-  pyproject-nix,
-  pyproject-build-systems,
-  uv2nix,
+  autoconf,
+  automake,
+  cmake,
+  clang,
+  k,
+  boost,
+  libtool,
+  mpfr,
+  openssl,
+  gmp,
+  pkg-config,
+  secp256k1,
+  which,
 
-  python
+  kontrol-node-pyk,
 }:
 let
-  pyproject-util = callPackage pyproject-nix.build.util {};
-  pyproject-packages = callPackage pyproject-nix.build.packages {
-    inherit python;
-  };
-
-  # load a uv workspace from a workspace root
-  workspace = uv2nix.lib.workspace.loadWorkspace {
-    workspaceRoot = lib.cleanSource (nix-gitignore.gitignoreSourcePure [
-        ../../.gitignore
-        ".github/"
-        "result*"
-        # do not include submodule directories that might be initilized empty or non-existent due to nix/git
-        # otherwise cachix build might not match the version that is requested by `kup`
-        # TODO: for new projects, add your submodule directories that are not required for nix builds here!
-        # e.g., `"/docs/external-computation"` with `external-computation` being a git submodule directory
-        # "/docs/external-computation"
-      ] ../..
-    );
-  };
-
-  # create overlay
-  lockFileOverlay = workspace.mkPyprojectOverlay {
-    # prefer "wheel" over "sdist" due to maintance overhead
-    # there is no bundled set of overlays for "sdist" in uv2nix, in contrast to poetry2nix
-    sourcePreference = "wheel";
-  };
-
-  buildSystemsOverlay = import ./build-systems-overlay.nix;
-
-  # construct package set
-  pythonSet = pyproject-packages.overrideScope (lib.composeManyExtensions [
-    # make build tools available by default as these are not necessarily specified in python lock files
-    pyproject-build-systems.overlays.default
-    # include all packages from the python lock file
-    lockFileOverlay
-    # add build system overrides to certain python packages
-    buildSystemsOverlay
-  ]);
-in pyproject-util.mkApplication {
-  # default dependancy group enables no optional dependencies and no dependency-groups
-  venv = pythonSet.mkVirtualEnv "kontrol-node-env" workspace.deps.default;
-  package = pythonSet.kontrol-node;
+  nixLibs = "-I${openssl.dev}/include -L${openssl.out}/lib -I${secp256k1}/include -L${secp256k1}/lib";
+in
+stdenv.mkDerivation {
+  pname = "kontrol-node";
+  inherit (kontrol-node-pyk) version;
+
+  # Everything is built from the Python package; there are no sources of our own.
+  dontUnpack = true;
+  dontUseCmakeConfigure = true;
+
+  buildInputs = [
+    autoconf
+    automake
+    cmake
+    clang
+    kontrol-node-pyk
+    k
+    boost
+    libtool
+    mpfr
+    openssl.dev
+    gmp
+    pkg-config
+    secp256k1
+    which
+  ];
+  nativeBuildInputs = [ makeWrapper ];
+
+  enableParallelBuilding = true;
+
+  # Build the semantics here so that `kontrol-node run` finds them prebuilt (via `KDIST_DIR`)
+  # instead of failing on the first request.
+  buildPhase = ''
+    runHook preBuild
+    export HOME=$(mktemp -d)
+    KDIST_DIR=$(pwd)/kdist NIX_LIBS="${nixLibs}" ${
+      lib.optionalString (stdenv.isAarch64 && stdenv.isDarwin) "APPLE_SILICON=true"
+    } ${kontrol-node-pyk.venv}/bin/kdist -v build kontrol-node.simbolik
+    runHook postBuild
+  '';
+
+  # Ship the matching K on PATH: `kontrol-node` checks the K version at startup, and must not pick
+  # up whatever K the user happens to have installed.
+  installPhase = ''
+    runHook preInstall
+    mkdir -p $out/bin
+    cp -r ./kdist $out/kdist
+    makeWrapper ${kontrol-node-pyk}/bin/kontrol-node $out/bin/kontrol-node \
+      --prefix PATH : ${lib.makeBinPath [ which k ]} \
+      --set NIX_LIBS "${nixLibs}" \
+      --set KDIST_DIR $out/kdist
+    runHook postInstall
+  '';
+
+  meta.mainProgram = "kontrol-node";
 }
diff --git a/src/kontrol_node/__main__.py b/src/kontrol_node/__main__.py
index 76f89f46..bfcd1242 100644
--- a/src/kontrol_node/__main__.py
+++ b/src/kontrol_node/__main__.py
@@ -70,7 +70,11 @@ def exec_version(options: VersionOptions) -> None:
 
 def exec_run(options: VMOptions) -> None:
     server = KontrolNodeServer(options)
-    server.serve()
+    try:
+        server.serve()
+    except RuntimeError as err:
+        _LOGGER.error(err)
+        sys.exit(1)
 
 
 if __name__ == '__main__':
diff --git a/src/kontrol_node/rpc.py b/src/kontrol_node/rpc.py
index 3c6a4f47..40ad3b20 100644
--- a/src/kontrol_node/rpc.py
+++ b/src/kontrol_node/rpc.py
@@ -28,6 +28,8 @@
 
 _DEBUG_KORE: Final[bool] = False
 
+_DEFINITION_TARGET: Final = 'kontrol-node.simbolik'
+
 # Simbolik needs at minimum the following RPC methods
 # eth_sendTransaction
 # eth_getTransactionByHash
@@ -53,12 +55,15 @@ class KontrolNodeServer:
 
     def __init__(self, options: VMOptions) -> None:
         self.options = options
-        print(f'Initialized KontrolNodeServer with options: {self.options}')
+        _LOGGER.info(f'Initialized KontrolNodeServer with options: {self.options}')
 
     def serve(self) -> None:
         _LOGGER.info(f'Starting JSON-RPC server at {self.options.addr}:{self.options.port}')
         self.handler, self.interpreter = create_handler()
         self.http_server = HTTPServer((self.options.addr, int(self.options.port)), self.handler)
+        # Flush explicitly: when stdout is not a TTY it is block-buffered, and callers waiting for
+        # this line to know the node is ready would otherwise never see it.
+        print(f'Listening on http://{self.options.addr}:{self.port()}', flush=True)
         self.http_server.serve_forever()
         _LOGGER.info(f'JSON-RPC server at {self.options.addr}:{self.options.port} shut down.')
 
@@ -83,8 +88,12 @@ class InterpreterProcess:
     """
 
     io_dir: Path
+    definition_dir: Path
 
     def __init__(self) -> None:
+        # Resolve the semantics before creating any state, so that a missing build fails at startup
+        # instead of on the first request.
+        self.definition_dir = _definition_dir()
         self._setup_io_dir()
         atexit.register(self.shutdown)
 
@@ -115,7 +124,7 @@ def _run(self) -> Pattern:
         if _DEBUG_KORE:
             with open('input.kore', 'w') as f:
                 f.write(initial_kore.text)
-        result = llvm_interpret(definition_dir=kdist.get('kontrol-node.simbolik'), pattern=initial_kore, check=False)
+        result = llvm_interpret(definition_dir=self.definition_dir, pattern=initial_kore, check=False)
         return result
 
     def request(self, payload: bytes) -> Path:
@@ -180,6 +189,17 @@ def _response_file(self) -> Path:
         return self.io_dir / 'response.json'
 
 
+def _definition_dir() -> Path:
+    definition_dir = kdist.get_or_none(_DEFINITION_TARGET)
+    if definition_dir is None:
+        raise RuntimeError(
+            f'The K semantics {_DEFINITION_TARGET} are not built (looked in {kdist.kdist_dir}). '
+            f'Build them with `kdist build {_DEFINITION_TARGET}`, '
+            'or reinstall with `kup install kontrol-node`, which ships them prebuilt.'
+        )
+    return definition_dir
+
+
 def create_handler() -> tuple[type[BaseHTTPRequestHandler], InterpreterProcess]:
 
     interpreter = InterpreterProcess()
@@ -196,12 +216,25 @@ def do_POST(self) -> None:  # noqa: N802
             assert type(content_len) is str
             content = self.rfile.read(int(content_len))
 
-            result_file = interpreter.request(content)
-            result_size = result_file.stat().st_size
+            try:
+                result_file = interpreter.request(content)
+            except Exception:
+                # Answer with an error instead of dropping the connection, which clients see as a hang.
+                _LOGGER.exception('Failed to process request')
+                self._send_json(
+                    json.dumps(
+                        {
+                            'jsonrpc': '2.0',
+                            'id': None,
+                            'error': {'code': -32603, 'message': 'Internal error'},
+                        }
+                    ).encode('utf-8')
+                )
+                return
 
             self.send_response(200)
             self.send_header('Content-Type', 'application/json')
-            self.send_header('Content-Length', str(result_size))
+            self.send_header('Content-Length', str(result_file.stat().st_size))
             self.end_headers()
 
             with open(result_file, 'rb') as f:
@@ -213,6 +246,13 @@ def do_POST(self) -> None:  # noqa: N802
                 filename = f'profiling/profiling-{transaction_hash}.prof'
                 profile.dump_stats(filename)
 
+        def _send_json(self, body: bytes) -> None:
+            self.send_response(200)
+            self.send_header('Content-Type', 'application/json')
+            self.send_header('Content-Length', str(len(body)))
+            self.end_headers()
+            self.wfile.write(body)
+
     return (KontrolNodeHandler, interpreter)
 
 

From ad95012e97f22f890e4dc6fd874d28e132279f9d Mon Sep 17 00:00:00 2001
From: Raoul <raoul.schaffranek@runtimeverification.com>
Date: Tue, 13 Oct 2026 12:48:29 +0000
Subject: [PATCH 2/4] Follow best practices from kontrol

---
 flake.lock                             |  66 +++++----------
 flake.nix                              | 112 ++++++++++++++-----------
 nix/kontrol-node-pyk/default.nix       |  40 ++-------
 nix/kontrol-node-pyproject/default.nix |  20 +++++
 nix/kontrol-node-source/default.nix    |  17 ++++
 nix/kontrol-node/default.nix           |  47 +++++------
 pyproject.toml                         |   1 +
 7 files changed, 150 insertions(+), 153 deletions(-)
 create mode 100644 nix/kontrol-node-pyproject/default.nix
 create mode 100644 nix/kontrol-node-source/default.nix

diff --git a/flake.lock b/flake.lock
index 8c9ec562..f66828c2 100644
--- a/flake.lock
+++ b/flake.lock
@@ -182,25 +182,7 @@
     },
     "flake-utils_2": {
       "inputs": {
-        "systems": "systems_2"
-      },
-      "locked": {
-        "lastModified": 1731533236,
-        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
-        "type": "github"
-      },
-      "original": {
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "type": "github"
-      }
-    },
-    "flake-utils_3": {
-      "inputs": {
-        "systems": "systems_4"
+        "systems": "systems_3"
       },
       "locked": {
         "lastModified": 1710146030,
@@ -216,9 +198,9 @@
         "type": "github"
       }
     },
-    "flake-utils_4": {
+    "flake-utils_3": {
       "inputs": {
-        "systems": "systems_6"
+        "systems": "systems_5"
       },
       "locked": {
         "lastModified": 1731533236,
@@ -296,7 +278,7 @@
     },
     "haskell-backend": {
       "inputs": {
-        "flake-utils": "flake-utils_2",
+        "flake-utils": "flake-utils",
         "nixpkgs": [
           "kontrol",
           "kevm",
@@ -333,7 +315,7 @@
     },
     "haskell-backend_2": {
       "inputs": {
-        "flake-utils": "flake-utils_4",
+        "flake-utils": "flake-utils_3",
         "nixpkgs": [
           "kontrol",
           "kevm",
@@ -858,7 +840,7 @@
     },
     "poetry2nix": {
       "inputs": {
-        "flake-utils": "flake-utils_3",
+        "flake-utils": "flake-utils_2",
         "nix-github-actions": "nix-github-actions",
         "nixpkgs": [
           "kontrol",
@@ -868,7 +850,7 @@
           "llvm-backend",
           "nixpkgs"
         ],
-        "systems": "systems_5",
+        "systems": "systems_4",
         "treefmt-nix": "treefmt-nix"
       },
       "locked": {
@@ -1179,11 +1161,18 @@
     },
     "root": {
       "inputs": {
-        "flake-utils": "flake-utils",
+        "flake-utils": [
+          "kevm",
+          "flake-utils"
+        ],
         "k-framework": [
-          "kontrol",
+          "kevm",
           "k-framework"
         ],
+        "kevm": [
+          "kontrol",
+          "kevm"
+        ],
         "kontrol": "kontrol",
         "nixpkgs": [
           "rv-nix-tools",
@@ -1447,21 +1436,6 @@
       }
     },
     "systems_4": {
-      "locked": {
-        "lastModified": 1681028828,
-        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
-        "owner": "nix-systems",
-        "repo": "default",
-        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-systems",
-        "repo": "default",
-        "type": "github"
-      }
-    },
-    "systems_5": {
       "locked": {
         "lastModified": 1681028828,
         "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
@@ -1475,7 +1449,7 @@
         "type": "indirect"
       }
     },
-    "systems_6": {
+    "systems_5": {
       "locked": {
         "lastModified": 1681028828,
         "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
@@ -1490,7 +1464,7 @@
         "type": "github"
       }
     },
-    "systems_7": {
+    "systems_6": {
       "locked": {
         "lastModified": 1681028828,
         "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
@@ -1532,7 +1506,7 @@
     },
     "utils": {
       "inputs": {
-        "systems": "systems_3"
+        "systems": "systems_2"
       },
       "locked": {
         "lastModified": 1705309234,
@@ -1550,7 +1524,7 @@
     },
     "utils_2": {
       "inputs": {
-        "systems": "systems_7"
+        "systems": "systems_6"
       },
       "locked": {
         "lastModified": 1705309234,
diff --git a/flake.nix b/flake.nix
index 97ee6ef6..2fe99d69 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,5 +1,6 @@
 {
   description = "kontrol-node - A local testnet node powered by KEVM";
+
   inputs = {
     rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/854d4f05ea78547d46e807b414faad64cea10ae4";
     nixpkgs.follows = "rv-nix-tools/nixpkgs";
@@ -7,10 +8,9 @@
     kontrol.url = "github:runtimeverification/kontrol/v1.0.213";
     kontrol.inputs.nixpkgs.follows = "nixpkgs";
 
-    k-framework.follows = "kontrol/k-framework";
-    k-framework.inputs.nixpkgs.follows = "nixpkgs";
-
-    flake-utils.url = "github:numtide/flake-utils";
+    kevm.follows = "kontrol/kevm";
+    k-framework.follows = "kevm/k-framework";
+    flake-utils.follows = "kevm/flake-utils";
     uv2nix.url = "github:pyproject-nix/uv2nix/4cca323a547a1aaa9b94929c4901bed5343eafe8";
     # uv2nix requires a newer version of nixpkgs
     # therefore, we pin uv2nix specifically to a newer version of nixpkgs
@@ -28,16 +28,22 @@
     };
     pyproject-nix.follows = "uv2nix/pyproject-nix";
   };
-  outputs = { self, rv-nix-tools, nixpkgs, kontrol, k-framework, flake-utils, pyproject-nix, pyproject-build-systems, uv2nix, nixpkgs-unstable }:
+  outputs = {
+      self,
+      k-framework,
+      nixpkgs,
+      flake-utils,
+      kevm,
+      kontrol,
+      rv-nix-tools,
+      pyproject-nix,
+      pyproject-build-systems,
+      uv2nix,
+      nixpkgs-unstable,
+      ... }:
   let
     pythonVer = "310";
-    nixLibs = pkgs: with pkgs; "-I${openssl.dev}/include -L${openssl.out}/lib -I${secp256k1}/include -L${secp256k1}/lib";
-  in flake-utils.lib.eachSystem [
-      "x86_64-linux"
-      "x86_64-darwin"
-      "aarch64-linux"
-      "aarch64-darwin"
-    ] (system:
+  in flake-utils.lib.eachDefaultSystem (system:
     let
       pkgs-unstable = import nixpkgs-unstable {
         inherit system;
@@ -47,73 +53,81 @@
         inherit (pkgs-unstable) replaceVars;
       };
       # due to the nixpkgs that we use in this flake being outdated, uv is also heavily outdated
-      # we can instead use the binary release of uv provided by uv2nix for now
+      # we can just use the binary release of uv provided by uv2nix
       uvOverlay = final: prev: {
         uv = uv2nix.packages.${final.system}.uv-bin;
       };
-      kOverlay = final: prev: {
-        k = k-framework.packages.${system}.k;
-      };
-      kontrol-nodeOverlay = final: prev: {
+      kontrol-nodeOverlay = final: prev:
+      let
+        kontrol-node-pyproject = final.callPackage ./nix/kontrol-node-pyproject {
+          inherit uv2nix;
+        };
         kontrol-node-pyk = final.callPackage ./nix/kontrol-node-pyk {
-          inherit pyproject-nix pyproject-build-systems uv2nix;
+          inherit pyproject-nix pyproject-build-systems kontrol-node-pyproject;
+          pyproject-overlays = [
+            (k-framework.overlays.pyk-pyproject system)
+            (kevm.overlays.pyk-pyproject system)
+            # `kontrol.overlays.pyk-pyproject` overrides `kontrol-pyk`, which is not a python package,
+            # so it would leave `kontrol` from `uv.lock` in place; override the right package instead
+            (final: prev: {
+              inherit (kontrol.packages.${system}.kontrol-pyk-pyproject.lockFileOverlay final prev) kontrol;
+            })
+          ];
           python = final."python${pythonVer}";
         };
-        kontrol-node = final.callPackage ./nix/kontrol-node { };
+        kontrol-node = final.callPackage ./nix/kontrol-node {
+          inherit kontrol-node-pyk;
+          rev = self.rev or null;
+        };
+      in {
+        inherit kontrol-node kontrol-node-pyk kontrol-node-pyproject;
       };
       pkgs = import nixpkgs {
         inherit system;
         overlays = [
           staleNixpkgsOverlay
+          (final: prev: { llvm-backend-release = false; })
+          k-framework.overlay
+          kevm.overlays.default
           uvOverlay
-          kOverlay
           kontrol-nodeOverlay
         ];
       };
       python = pkgs."python${pythonVer}";
     in {
-      devShells.default = pkgs.mkShell {
-        name = "uv develop shell";
-        packages = with pkgs; ([
-          k
-          autoconf
-          automake
-          cmake
-          pkg-config
+      devShells.default =
+      let
+        kevmShell = kevm.devShells.${system}.default;
+      in pkgs.mkShell {
+        # kevm's shell lists K and the build tools in `packages`, which end up in `nativeBuildInputs`
+        nativeBuildInputs = kevmShell.nativeBuildInputs or [ ];
+        buildInputs = (kevmShell.buildInputs or [ ]) ++ [
           python
-          clang
-          uv
-          which
-        ] ++ lib.optionals (!stdenv.isDarwin) [
-          elfutils
-        ]);
-        buildInputs = with pkgs; [
-          fmt
-          libtool
-          mpfr
-          openssl
-          secp256k1
-          boost
+          pkgs.uv
         ];
-        env = {
+        env = (kevmShell.env or { }) // {
           # prevent uv from managing Python downloads and force use of specific
           UV_PYTHON_DOWNLOADS = "never";
           UV_PYTHON = python.interpreter;
         };
-        shellHook = ''
-          export NIX_LIBS="${nixLibs pkgs}"
+        shellHook = (kevmShell.shellHook or "") + ''
           unset PYTHONPATH
-        '' + pkgs.lib.strings.optionalString (pkgs.stdenv.isAarch64 && pkgs.stdenv.isDarwin) ''
-          export APPLE_SILICON=true
         '';
       };
       packages = rec {
-        inherit (pkgs) kontrol-node kontrol-node-pyk;
+        inherit (pkgs) kontrol-node kontrol-node-pyk kontrol-node-pyproject;
         default = kontrol-node;
       };
     }) // {
-      overlays.default = final: prev: {
-        inherit (self.packages.${final.system}) kontrol-node;
+      overlays = {
+        default = final: prev: {
+          inherit (self.packages.${final.system}) kontrol-node;
+        };
+        # this pyproject-nix overlay allows for overriding the python packages that are otherwise locked in `uv.lock`
+        # by using this overlay in dependant nix flakes, you ensure that nix overrides also override the python package
+        pyk-pyproject = system: final: prev: {
+          inherit (self.packages.${system}.kontrol-node-pyproject.lockFileOverlay final prev) kontrol-node;
+        };
       };
     };
 }
diff --git a/nix/kontrol-node-pyk/default.nix b/nix/kontrol-node-pyk/default.nix
index a949dffc..e5396eec 100644
--- a/nix/kontrol-node-pyk/default.nix
+++ b/nix/kontrol-node-pyk/default.nix
@@ -1,59 +1,35 @@
 {
   lib,
   callPackage,
-  nix-gitignore,
 
   pyproject-nix,
   pyproject-build-systems,
-  uv2nix,
+  kontrol-node-pyproject,
+  pyproject-overlays ? [ ],
 
   python
 }:
 let
+  inherit (kontrol-node-pyproject) lockFileOverlay workspace;
+
   pyproject-util = callPackage pyproject-nix.build.util {};
   pyproject-packages = callPackage pyproject-nix.build.packages {
     inherit python;
   };
 
-  # load a uv workspace from a workspace root
-  workspace = uv2nix.lib.workspace.loadWorkspace {
-    workspaceRoot = lib.cleanSource (nix-gitignore.gitignoreSourcePure [
-        ../../.gitignore
-        ".github/"
-        "result*"
-        # do not include submodule directories that might be initilized empty or non-existent due to nix/git
-        # otherwise cachix build might not match the version that is requested by `kup`
-        # TODO: for new projects, add your submodule directories that are not required for nix builds here!
-        # e.g., `"/docs/external-computation"` with `external-computation` being a git submodule directory
-        # "/docs/external-computation"
-      ] ../..
-    );
-  };
-
-  # create overlay
-  lockFileOverlay = workspace.mkPyprojectOverlay {
-    # prefer "wheel" over "sdist" due to maintance overhead
-    # there is no bundled set of overlays for "sdist" in uv2nix, in contrast to poetry2nix
-    sourcePreference = "wheel";
-  };
-
   buildSystemsOverlay = import ./build-systems-overlay.nix;
 
   # construct package set
-  pythonSet = pyproject-packages.overrideScope (lib.composeManyExtensions [
+  pythonSet = pyproject-packages.overrideScope (lib.composeManyExtensions ([
     # make build tools available by default as these are not necessarily specified in python lock files
     pyproject-build-systems.overlays.default
     # include all packages from the python lock file
     lockFileOverlay
     # add build system overrides to certain python packages
     buildSystemsOverlay
-  ]);
+  ] ++ pyproject-overlays));
+in pyproject-util.mkApplication {
   # default dependancy group enables no optional dependencies and no dependency-groups
   venv = pythonSet.mkVirtualEnv "kontrol-node-env" workspace.deps.default;
-in (pyproject-util.mkApplication {
-  inherit venv;
   package = pythonSet.kontrol-node;
-}).overrideAttrs (old: {
-  # the application only exposes `kontrol-node`; the venv also provides `kdist` to build the semantics
-  passthru = (old.passthru or { }) // { inherit venv; };
-})
+}
diff --git a/nix/kontrol-node-pyproject/default.nix b/nix/kontrol-node-pyproject/default.nix
new file mode 100644
index 00000000..cfe7a6fb
--- /dev/null
+++ b/nix/kontrol-node-pyproject/default.nix
@@ -0,0 +1,20 @@
+{
+  callPackage,
+
+  uv2nix,
+}:
+let
+  # load a uv workspace from a workspace root
+  workspace = uv2nix.lib.workspace.loadWorkspace {
+    workspaceRoot = callPackage ../kontrol-node-source { };
+  };
+
+  # create overlay
+  lockFileOverlay = workspace.mkPyprojectOverlay {
+    # prefer "wheel" over "sdist" due to maintenance overhead
+    # there is no bundled set of overlays for "sdist" in uv2nix, in contrast to poetry2nix
+    sourcePreference = "wheel";
+  };
+in {
+  inherit lockFileOverlay workspace;
+}
diff --git a/nix/kontrol-node-source/default.nix b/nix/kontrol-node-source/default.nix
new file mode 100644
index 00000000..8f0f559c
--- /dev/null
+++ b/nix/kontrol-node-source/default.nix
@@ -0,0 +1,17 @@
+{
+  lib,
+  nix-gitignore
+}:
+
+lib.cleanSource (nix-gitignore.gitignoreSourcePure [
+    ../../.gitignore
+    ".github/"
+    "result*"
+    "/deps/"
+    # do not include submodule directories that might be initilized empty or non-existent due to nix/git
+    # otherwise cachix build might not match the version that is requested by `kup`
+    # TODO: for new projects, add your submodule directories that are not required for nix builds here!
+    # e.g., `"/docs/external-computation"` with `external-computation` being a git submodule directory
+    # "/docs/external-computation"
+  ] ../../.
+)
diff --git a/nix/kontrol-node/default.nix b/nix/kontrol-node/default.nix
index caec1e3c..bb28dd11 100644
--- a/nix/kontrol-node/default.nix
+++ b/nix/kontrol-node/default.nix
@@ -2,6 +2,7 @@
   lib,
   stdenv,
   makeWrapper,
+  callPackage,
 
   autoconf,
   automake,
@@ -18,18 +19,14 @@
   which,
 
   kontrol-node-pyk,
+  rev ? null
 }:
 let
   nixLibs = "-I${openssl.dev}/include -L${openssl.out}/lib -I${secp256k1}/include -L${secp256k1}/lib";
 in
 stdenv.mkDerivation {
   pname = "kontrol-node";
-  inherit (kontrol-node-pyk) version;
-
-  # Everything is built from the Python package; there are no sources of our own.
-  dontUnpack = true;
-  dontUseCmakeConfigure = true;
-
+  version = if (rev != null) then rev else "dirty";
   buildInputs = [
     autoconf
     automake
@@ -44,35 +41,33 @@ stdenv.mkDerivation {
     gmp
     pkg-config
     secp256k1
-    which
   ];
   nativeBuildInputs = [ makeWrapper ];
 
+  src = callPackage ../kontrol-node-source { };
+
+  dontUseCmakeConfigure = true;
+
   enableParallelBuilding = true;
 
-  # Build the semantics here so that `kontrol-node run` finds them prebuilt (via `KDIST_DIR`)
-  # instead of failing on the first request.
+  # Build the semantics here so that `kontrol-node run` finds them prebuilt instead of failing on the
+  # first request.
   buildPhase = ''
-    runHook preBuild
-    export HOME=$(mktemp -d)
-    KDIST_DIR=$(pwd)/kdist NIX_LIBS="${nixLibs}" ${
-      lib.optionalString (stdenv.isAarch64 && stdenv.isDarwin) "APPLE_SILICON=true"
-    } ${kontrol-node-pyk.venv}/bin/kdist -v build kontrol-node.simbolik
-    runHook postBuild
+    XDG_CACHE_HOME=$(pwd) NIX_LIBS="${nixLibs}" ${
+      lib.optionalString
+      (stdenv.isAarch64 && stdenv.isDarwin)
+      "APPLE_SILICON=true"
+    } kontrol-node-kdist -v build kontrol-node.simbolik
   '';
 
-  # Ship the matching K on PATH: `kontrol-node` checks the K version at startup, and must not pick
-  # up whatever K the user happens to have installed.
+  # Ship the matching K on PATH: `kontrol-node` checks the K version at startup, and must not pick up
+  # whatever K the user happens to have installed.
   installPhase = ''
-    runHook preInstall
+    mkdir -p $out
+    cp -r ./kdist-*/* $out/
     mkdir -p $out/bin
-    cp -r ./kdist $out/kdist
-    makeWrapper ${kontrol-node-pyk}/bin/kontrol-node $out/bin/kontrol-node \
-      --prefix PATH : ${lib.makeBinPath [ which k ]} \
-      --set NIX_LIBS "${nixLibs}" \
-      --set KDIST_DIR $out/kdist
-    runHook postInstall
+    makeWrapper ${kontrol-node-pyk}/bin/kontrol-node $out/bin/kontrol-node --prefix PATH : ${
+      lib.makeBinPath [ which k ]
+    } --set NIX_LIBS "${nixLibs}" --set KDIST_DIR $out
   '';
-
-  meta.mainProgram = "kontrol-node";
 }
diff --git a/pyproject.toml b/pyproject.toml
index f7331280..10d387d7 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -19,6 +19,7 @@ email = "contact@runtimeverification.com"
 
 [project.scripts]
 kontrol-node = "kontrol_node.__main__:main"
+kontrol-node-kdist = "pyk.kdist.__main__:main"
 
 [project.entry-points.kdist]
 kontrol-node = "kontrol_node.kdist.plugin"

From 584fc219ba0466921cab3038846025124be0a158 Mon Sep 17 00:00:00 2001
From: Raoul <raoul.schaffranek@runtimeverification.com>
Date: Tue, 13 Oct 2026 13:02:41 +0000
Subject: [PATCH 3/4] Remove dead code

---
 flake.nix                                      | 13 ++++---------
 nix/kontrol-node-pyk/build-systems-overlay.nix |  3 ---
 nix/kontrol-node/default.nix                   |  4 +---
 3 files changed, 5 insertions(+), 15 deletions(-)

diff --git a/flake.nix b/flake.nix
index 2fe99d69..ef3259bb 100644
--- a/flake.nix
+++ b/flake.nix
@@ -35,7 +35,6 @@
       flake-utils,
       kevm,
       kontrol,
-      rv-nix-tools,
       pyproject-nix,
       pyproject-build-systems,
       uv2nix,
@@ -86,9 +85,7 @@
         inherit system;
         overlays = [
           staleNixpkgsOverlay
-          (final: prev: { llvm-backend-release = false; })
           k-framework.overlay
-          kevm.overlays.default
           uvOverlay
           kontrol-nodeOverlay
         ];
@@ -100,19 +97,17 @@
         kevmShell = kevm.devShells.${system}.default;
       in pkgs.mkShell {
         # kevm's shell lists K and the build tools in `packages`, which end up in `nativeBuildInputs`
-        nativeBuildInputs = kevmShell.nativeBuildInputs or [ ];
-        buildInputs = (kevmShell.buildInputs or [ ]) ++ [
+        nativeBuildInputs = kevmShell.nativeBuildInputs;
+        buildInputs = kevmShell.buildInputs ++ [
           python
           pkgs.uv
         ];
-        env = (kevmShell.env or { }) // {
+        env = {
           # prevent uv from managing Python downloads and force use of specific
           UV_PYTHON_DOWNLOADS = "never";
           UV_PYTHON = python.interpreter;
         };
-        shellHook = (kevmShell.shellHook or "") + ''
-          unset PYTHONPATH
-        '';
+        inherit (kevmShell) shellHook;
       };
       packages = rec {
         inherit (pkgs) kontrol-node kontrol-node-pyk kontrol-node-pyproject;
diff --git a/nix/kontrol-node-pyk/build-systems-overlay.nix b/nix/kontrol-node-pyk/build-systems-overlay.nix
index 7567b17f..a906530d 100644
--- a/nix/kontrol-node-pyk/build-systems-overlay.nix
+++ b/nix/kontrol-node-pyk/build-systems-overlay.nix
@@ -10,9 +10,6 @@ let
   # `setuptools-scm[toml]` in pyproject.toml would be written as
   # `foo.setuptools-scm = [ "toml" ]` in Nix
   buildSystemOverrides = {
-    # git dependencies are built from source, but uv.lock does not record their build systems
-    kevm-pyk.hatchling = [ ];
-    kontrol.hatchling = [ ];
     # sdist-only on PyPI
     typing.setuptools = [ ];
   };
diff --git a/nix/kontrol-node/default.nix b/nix/kontrol-node/default.nix
index bb28dd11..7d99bef9 100644
--- a/nix/kontrol-node/default.nix
+++ b/nix/kontrol-node/default.nix
@@ -48,8 +48,6 @@ stdenv.mkDerivation {
 
   dontUseCmakeConfigure = true;
 
-  enableParallelBuilding = true;
-
   # Build the semantics here so that `kontrol-node run` finds them prebuilt instead of failing on the
   # first request.
   buildPhase = ''
@@ -68,6 +66,6 @@ stdenv.mkDerivation {
     mkdir -p $out/bin
     makeWrapper ${kontrol-node-pyk}/bin/kontrol-node $out/bin/kontrol-node --prefix PATH : ${
       lib.makeBinPath [ which k ]
-    } --set NIX_LIBS "${nixLibs}" --set KDIST_DIR $out
+    } --set KDIST_DIR $out
   '';
 }

From ee65f9259705a2dbfe4100ea21bf140b715566af Mon Sep 17 00:00:00 2001
From: Raoul <raoul.schaffranek@runtimeverification.com>
Date: Tue, 13 Oct 2026 13:18:51 +0000
Subject: [PATCH 4/4] Address reviewer feedback.

---
 src/kontrol_node/__main__.py |  4 ++--
 src/kontrol_node/rpc.py      | 25 ++++++++-----------------
 2 files changed, 10 insertions(+), 19 deletions(-)

diff --git a/src/kontrol_node/__main__.py b/src/kontrol_node/__main__.py
index bfcd1242..5574e235 100644
--- a/src/kontrol_node/__main__.py
+++ b/src/kontrol_node/__main__.py
@@ -12,7 +12,7 @@
 
 from . import VERSION
 from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
-from .rpc import KontrolNodeServer
+from .rpc import KontrolNodeServer, SemanticsNotBuiltError
 
 if TYPE_CHECKING:
     from typing import Final, TypeVar
@@ -72,7 +72,7 @@ def exec_run(options: VMOptions) -> None:
     server = KontrolNodeServer(options)
     try:
         server.serve()
-    except RuntimeError as err:
+    except SemanticsNotBuiltError as err:
         _LOGGER.error(err)
         sys.exit(1)
 
diff --git a/src/kontrol_node/rpc.py b/src/kontrol_node/rpc.py
index 40ad3b20..4b6295f5 100644
--- a/src/kontrol_node/rpc.py
+++ b/src/kontrol_node/rpc.py
@@ -189,10 +189,14 @@ def _response_file(self) -> Path:
         return self.io_dir / 'response.json'
 
 
+class SemanticsNotBuiltError(RuntimeError):
+    pass
+
+
 def _definition_dir() -> Path:
     definition_dir = kdist.get_or_none(_DEFINITION_TARGET)
     if definition_dir is None:
-        raise RuntimeError(
+        raise SemanticsNotBuiltError(
             f'The K semantics {_DEFINITION_TARGET} are not built (looked in {kdist.kdist_dir}). '
             f'Build them with `kdist build {_DEFINITION_TARGET}`, '
             'or reinstall with `kup install kontrol-node`, which ships them prebuilt.'
@@ -221,16 +225,10 @@ def do_POST(self) -> None:  # noqa: N802
             except Exception:
                 # Answer with an error instead of dropping the connection, which clients see as a hang.
                 _LOGGER.exception('Failed to process request')
-                self._send_json(
-                    json.dumps(
-                        {
-                            'jsonrpc': '2.0',
-                            'id': None,
-                            'error': {'code': -32603, 'message': 'Internal error'},
-                        }
-                    ).encode('utf-8')
+                result_file = interpreter._response_file()
+                result_file.write_text(
+                    json.dumps({'jsonrpc': '2.0', 'id': None, 'error': {'code': -32603, 'message': 'Internal error'}})
                 )
-                return
 
             self.send_response(200)
             self.send_header('Content-Type', 'application/json')
@@ -246,13 +244,6 @@ def do_POST(self) -> None:  # noqa: N802
                 filename = f'profiling/profiling-{transaction_hash}.prof'
                 profile.dump_stats(filename)
 
-        def _send_json(self, body: bytes) -> None:
-            self.send_response(200)
-            self.send_header('Content-Type', 'application/json')
-            self.send_header('Content-Length', str(len(body)))
-            self.end_headers()
-            self.wfile.write(body)
-
     return (KontrolNodeHandler, interpreter)