From f072fc390e4e9d59634c04e290c4432e6422f722 Mon Sep 17 00:00:00 2001
From: Skot <48910715+saikatchatrg@users.noreply.github.com>
Date: Sat, 24 Oct 2026 12:36:40 +0200
Subject: [PATCH 01/13] build_openroad: install kepler-formal with a relative
 RUNPATH

The absolute RUNPATH tied bin/kepler-formal to the directory it was
built in, so a moved or re-pointed checkout loaded another build's
libnaja_*.so. Use $ORIGIN/../lib, and @loader_path/../lib on macOS.

Fixes #4717.

Signed-off-by: Skot <48910715+saikatchatrg@users.noreply.github.com>
---
 build_openroad.sh | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/build_openroad.sh b/build_openroad.sh
index 0eef046bd5..c92c0fc9c4 100755
--- a/build_openroad.sh
+++ b/build_openroad.sh
@@ -429,16 +429,23 @@ __local_build()
         # EL9 ships TBB 2020, where concurrent_map needs
         # TBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS; oneTBB ignores it.
         # EL installs libraries in lib64 by default; the RPATH points to lib.
+        # The RPATH is relative to bin/, so a moved install still loads its
+        # own libraries (#4717); macOS spells $ORIGIN as @loader_path.
         case "$(uname -m)" in
                 aarch64|arm64) KEPLER_MARCH="-march=armv8-a" ;;
                 *) KEPLER_MARCH="-march=x86-64-v3" ;;
         esac
+        if [[ "$OSTYPE" == "darwin"* ]]; then
+                KEPLER_RPATH="@loader_path/../lib"
+        else
+                KEPLER_RPATH="\$ORIGIN/../lib"
+        fi
         ${NICE} cmake -B tools/kepler-formal/build tools/kepler-formal \
                 -DCMAKE_BUILD_TYPE=Release \
                 -DCMAKE_CXX_FLAGS_RELEASE="-Ofast ${KEPLER_MARCH} -ffast-math -flto -DTBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS=1" \
                 -DCMAKE_EXE_LINKER_FLAGS="-flto" \
                 -DCMAKE_BUILD_RPATH="${DIR}/tools/kepler-formal/build/thirdparty/naja/src/dnl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/nl/nl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/optimization" \
-                -DCMAKE_INSTALL_RPATH="${INSTALL_PATH}/kepler-formal/lib" \
+                -DCMAKE_INSTALL_RPATH="${KEPLER_RPATH}" \
                 -DCMAKE_INSTALL_LIBDIR=lib \
                 -DCMAKE_BUILD_WITH_INSTALL_RPATH=OFF \
                 -DCMAKE_INSTALL_RPATH_USE_LINK_PATH=OFF \

From 21f71019667e2a6ddebd4b8bbefbb915e275c118 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Sun, 25 Oct 2026 07:09:24 +0100
Subject: [PATCH 02/13] etc/kepler-formal: pin kepler-formal and install it
 with one command
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A small Bazel module that only pins kepler-formal; ORFS itself does not
become a Bazel project. From this folder,

    bazelisk run //:install -- <prefix>

installs bin/kepler-formal with everything it loads next to it.
Bumping kepler-formal is the version line in MODULE.bazel. README.md
says how this maps to DependencyInstaller.sh, and which lines go away
as kepler-formal's registry entry and install target merge upstream.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 .gitignore                      |  2 ++
 etc/kepler-formal/.bazelrc      |  9 ++++++++
 etc/kepler-formal/.bazelversion |  1 +
 etc/kepler-formal/BUILD.bazel   |  5 +++++
 etc/kepler-formal/MODULE.bazel  | 29 ++++++++++++++++++++++++
 etc/kepler-formal/README.md     | 39 +++++++++++++++++++++++++++++++++
 6 files changed, 85 insertions(+)
 create mode 100644 etc/kepler-formal/.bazelrc
 create mode 100644 etc/kepler-formal/.bazelversion
 create mode 100644 etc/kepler-formal/BUILD.bazel
 create mode 100644 etc/kepler-formal/MODULE.bazel
 create mode 100644 etc/kepler-formal/README.md

diff --git a/.gitignore b/.gitignore
index 84d1e39569..afa12adbe8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -104,6 +104,8 @@ bazel-out
 bazel-OpenROAD-flow-scripts
 bazel-testlogs
 MODULE.bazel.lock
+# etc/kepler-formal
+bazel-kepler-formal
 
 # python venv
 venv/
diff --git a/etc/kepler-formal/.bazelrc b/etc/kepler-formal/.bazelrc
new file mode 100644
index 0000000000..bfb1b9cd74
--- /dev/null
+++ b/etc/kepler-formal/.bazelrc
@@ -0,0 +1,9 @@
+common --registry=https://bcr.bazel.build/
+
+build --cxxopt=-std=c++20
+build --host_cxxopt=-std=c++20
+build -c opt
+
+# As kepler-formal's own .bazelrc.
+common --enable_platform_specific_config
+build:linux --dynamic_mode=off
diff --git a/etc/kepler-formal/.bazelversion b/etc/kepler-formal/.bazelversion
new file mode 100644
index 0000000000..acd405b1d6
--- /dev/null
+++ b/etc/kepler-formal/.bazelversion
@@ -0,0 +1 @@
+8.6.0
diff --git a/etc/kepler-formal/BUILD.bazel b/etc/kepler-formal/BUILD.bazel
new file mode 100644
index 0000000000..4e4dc28d27
--- /dev/null
+++ b/etc/kepler-formal/BUILD.bazel
@@ -0,0 +1,5 @@
+# bazelisk run //:install -- <prefix>
+alias(
+    name = "install",
+    actual = "@kepler-formal//:install",
+)
diff --git a/etc/kepler-formal/MODULE.bazel b/etc/kepler-formal/MODULE.bazel
new file mode 100644
index 0000000000..975f111008
--- /dev/null
+++ b/etc/kepler-formal/MODULE.bazel
@@ -0,0 +1,29 @@
+"""Pins the kepler-formal that build_openroad.sh installs.
+
+ORFS is not a Bazel project: this module exists only to install
+kepler-formal into tools/install/kepler-formal. See README.md.
+"""
+
+module(name = "orfs-kepler-formal")
+
+# To bump kepler-formal, change this version.
+bazel_dep(name = "kepler-formal", version = "0.5.0-20261020-0be91596")
+
+# TODO(keplertech/kepler-formal#292): delete this override once a
+# kepler-formal version with the //:install target is on the registry,
+# and move the version above to it.
+git_override(
+    module_name = "kepler-formal",
+    commit = "99d66cac88978312853a10b82657781f8e99d843",
+    remote = "https://github.com/oharboe/kepler-formal.git",
+)
+
+# kepler-formal builds with a downloaded clang. It registers that
+# toolchain for its own builds only, so a module that depends on it
+# registers it too. Elsewhere the host compiler is used.
+bazel_dep(name = "llvm", version = "0.8.24")
+
+llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain")
+use_repo(llvm_toolchains, "llvm_toolchains")
+
+register_toolchains("@llvm_toolchains//:all")
diff --git a/etc/kepler-formal/README.md b/etc/kepler-formal/README.md
new file mode 100644
index 0000000000..9b7495f429
--- /dev/null
+++ b/etc/kepler-formal/README.md
@@ -0,0 +1,39 @@
+# kepler-formal
+
+To bump kepler-formal, change the version in `MODULE.bazel`.
+
+`build_openroad.sh --local` installs kepler-formal into
+`tools/install/kepler-formal/bin/kepler-formal` from this folder:
+
+```shell
+cd etc/kepler-formal
+bazelisk run //:install -- "$(pwd)/../../tools/install/kepler-formal"
+```
+
+ORFS is not a Bazel project. This folder only pins kepler-formal; the
+install is kepler-formal's own `//:install` target.
+
+## How this maps to `DependencyInstaller.sh`
+
+`DependencyInstaller.sh` downloads a pinned CMake from Kitware when the
+one the OS ships is too old, and checks it against a checksum. Bazel
+does the same for kepler-formal and every library it needs, from the
+[Bazel Central Registry](https://registry.bazel.build/), which keeps the
+URL, the checksum and the build file of each version:
+
+| `DependencyInstaller.sh`, `build_openroad.sh` | Here |
+| --- | --- |
+| oneTBB and capnproto from the OS, or built from a pinned tarball | `bazel_dep` versions in kepler-formal's `MODULE.bazel` |
+| A pinned CMake when the OS's is too old | bazelisk runs the Bazel named in `.bazelversion` |
+| `gcc-toolset-13` on EL8, because GCC 8 is too old | A pinned clang is downloaded on x86-64 Linux; elsewhere the host compiler is used |
+| `tools/kepler-formal` and the submodules inside it | The version in `MODULE.bazel`; sources are checked against their checksums and cached in `~/.cache/bazel` |
+| An RPATH that points at the install's `lib/` | The binary finds its libraries next to itself, in `bin/kepler-formal.runfiles/` |
+
+## What goes away as upstream merges
+
+1. When a registry version of kepler-formal has the install target
+   (keplertech/kepler-formal#292, after
+   bazelbuild/bazel-central-registry#11201): delete the `git_override` in
+   `MODULE.bazel` and move the version to it.
+2. When kepler-formal registers its compiler for modules that depend on
+   it: delete the toolchain lines in `MODULE.bazel`.

From 513e51069aeb51ba728143ed9e35cb1b5d66720d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Sun, 25 Oct 2026 07:09:32 +0100
Subject: [PATCH 03/13] build_openroad: install kepler-formal from
 etc/kepler-formal
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Instead of building kepler-formal with CMake, run its install target
from etc/kepler-formal, as Build.sh already builds OpenROAD with Bazel.
This drops the per-architecture -march choice, the EL9 TBB define, the
LTO flags, the build and install RPATHs (#4717) and the gcc-toolset-13
setup that only kepler-formal needed. The binary still lands in
tools/install/kepler-formal/bin/kepler-formal, and it loads its
libraries from next to itself, wherever the install is moved.

The Docker builder copies etc/kepler-formal into the image, and the
tools image tag covers it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 .dockerignore             |  3 +++
 build_openroad.sh         | 45 +++++++++++----------------------------
 docker/Dockerfile.builder |  1 +
 etc/DockerTag.sh          |  5 ++++-
 4 files changed, 20 insertions(+), 34 deletions(-)

diff --git a/.dockerignore b/.dockerignore
index e1a31f4e72..8395ed3302 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -1,6 +1,9 @@
 # Build working directories
 tools/OpenROAD/build/
 tools/kepler-formal/build/
+# Local Bazel outputs; the image builds its own.
+etc/kepler-formal/bazel-*
+etc/kepler-formal/MODULE.bazel.lock
 
 # Build files
 build_openroad.log
diff --git a/build_openroad.sh b/build_openroad.sh
index c92c0fc9c4..580a6f9ce9 100755
--- a/build_openroad.sh
+++ b/build_openroad.sh
@@ -385,12 +385,6 @@ __local_build()
                 source /opt/rh/devtoolset-8/enable
                 set -u
         fi
-        # EL8: the default GCC 8 is too old for kepler-formal.
-        if [[ -f "/opt/rh/gcc-toolset-13/enable" ]]; then
-                set +u
-                source /opt/rh/gcc-toolset-13/enable
-                set -u
-        fi
 
         if [ -z "${SKIP_OPENROAD+x}" ]; then
                 echo "[INFO FLW-0018] Compiling OpenROAD."
@@ -423,34 +417,19 @@ __local_build()
                 ${YOSYS_ARGS}
         ${NICE} cmake --build tools/yosys/build --target install -j "${PROC}"
 
-        echo "[INFO FLW-0031] Compiling kepler-formal"
-        # -march=x86-64-v3 is valid only for x86 compilers. On Arm, use the
-        # Armv8-A baseline, so that the binary runs on any aarch64 machine.
-        # EL9 ships TBB 2020, where concurrent_map needs
-        # TBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS; oneTBB ignores it.
-        # EL installs libraries in lib64 by default; the RPATH points to lib.
-        # The RPATH is relative to bin/, so a moved install still loads its
-        # own libraries (#4717); macOS spells $ORIGIN as @loader_path.
-        case "$(uname -m)" in
-                aarch64|arm64) KEPLER_MARCH="-march=armv8-a" ;;
-                *) KEPLER_MARCH="-march=x86-64-v3" ;;
-        esac
-        if [[ "$OSTYPE" == "darwin"* ]]; then
-                KEPLER_RPATH="@loader_path/../lib"
-        else
-                KEPLER_RPATH="\$ORIGIN/../lib"
+        echo "[INFO FLW-0031] Installing kepler-formal"
+        # etc/kepler-formal pins kepler-formal; Bazel downloads it, its
+        # dependencies and the compiler. See etc/kepler-formal/README.md.
+        if ! command -v bazelisk &> /dev/null; then
+                echo "[ERROR FLW-0034] kepler-formal needs bazelisk; run etc/DependencyInstaller.sh -common." >&2
+                exit 1
         fi
-        ${NICE} cmake -B tools/kepler-formal/build tools/kepler-formal \
-                -DCMAKE_BUILD_TYPE=Release \
-                -DCMAKE_CXX_FLAGS_RELEASE="-Ofast ${KEPLER_MARCH} -ffast-math -flto -DTBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS=1" \
-                -DCMAKE_EXE_LINKER_FLAGS="-flto" \
-                -DCMAKE_BUILD_RPATH="${DIR}/tools/kepler-formal/build/thirdparty/naja/src/dnl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/nl/nl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/optimization" \
-                -DCMAKE_INSTALL_RPATH="${KEPLER_RPATH}" \
-                -DCMAKE_INSTALL_LIBDIR=lib \
-                -DCMAKE_BUILD_WITH_INSTALL_RPATH=OFF \
-                -DCMAKE_INSTALL_RPATH_USE_LINK_PATH=OFF \
-                -DCMAKE_INSTALL_PREFIX="${INSTALL_PATH}/kepler-formal"
-        ${NICE} cmake --build tools/kepler-formal/build --target install -j "${PROC}"
+        KEPLER_PREFIX="${INSTALL_PATH}/kepler-formal"
+        if [[ "${KEPLER_PREFIX}" != /* ]]; then
+                KEPLER_PREFIX="$(pwd)/${KEPLER_PREFIX}"
+        fi
+        (cd "${DIR}/etc/kepler-formal" && \
+                ${NICE} bazelisk run --jobs="${PROC}" //:install -- "${KEPLER_PREFIX}")
 
         if [ ${WITH_VERIFIC} -eq 1 ]; then
                 echo "[INFO FLW-0032] Cleaning up Verific components."
diff --git a/docker/Dockerfile.builder b/docker/Dockerfile.builder
index 93ef32bec6..8ec79e6c7f 100644
--- a/docker/Dockerfile.builder
+++ b/docker/Dockerfile.builder
@@ -30,6 +30,7 @@ FROM orfs-builder-base AS orfs-tools-builder
 # Exclude install so a local build's output (e.g. tools/install/OpenROAD)
 # cannot leak into the image; the build below starts from an empty install.
 COPY --link --exclude=OpenROAD --exclude=AutoTuner --exclude=install tools tools
+COPY --link etc/kepler-formal etc/kepler-formal
 ARG numThreads=$(nproc)
 ARG verificPath=""
 
diff --git a/etc/DockerTag.sh b/etc/DockerTag.sh
index 315392c44d..5a4763da8e 100755
--- a/etc/DockerTag.sh
+++ b/etc/DockerTag.sh
@@ -16,7 +16,8 @@ if [[ "$@" == "-dev" ]]; then
 elif [[ "$@" == "-tools" ]]; then
     # Everything the orfs-tools target of Dockerfile.builder depends on:
     # the dev image, the build scripts, the ignore file that filters the
-    # build context, and the checked-out tools except OpenROAD.
+    # build context, the checked-out tools except OpenROAD, and the
+    # pinned kepler-formal.
     ignore_file=./docker/Dockerfile.builder.dockerignore
     if [[ ! -f "${ignore_file}" ]]; then
         ignore_file=./.dockerignore
@@ -29,6 +30,8 @@ elif [[ "$@" == "-tools" ]]; then
         git submodule status tools/yosys tools/kepler-formal | awk '{print $1, $2}'
         git ls-tree HEAD tools/ | grep -v -e 'tools/OpenROAD$' -e 'tools/AutoTuner$' \
             -e 'tools/yosys$' -e 'tools/kepler-formal$'
+        # The kepler-formal version and the Bazel settings that install it.
+        git ls-tree -r HEAD etc/kepler-formal
     } | sha256sum | awk '{print substr($1, 1, 6)}'
 elif [[ "$@" == "-master" ]]; then
     git fetch --tags >&2

From a92b10c151f018fb64fbc22dc6194e8e20db2a09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Sun, 25 Oct 2026 07:09:38 +0100
Subject: [PATCH 04/13] Remove the tools/kepler-formal submodule
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

build_openroad.sh installs kepler-formal from the version pinned in
etc/kepler-formal, so the submodule, and the five submodules inside
it, are no longer checked out. Its build directory leaves
.dockerignore and its commit leaves the tools image tag.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 .dockerignore       | 1 -
 .gitmodules         | 3 ---
 etc/DockerTag.sh    | 4 ++--
 tools/kepler-formal | 1 -
 4 files changed, 2 insertions(+), 7 deletions(-)
 delete mode 160000 tools/kepler-formal

diff --git a/.dockerignore b/.dockerignore
index 8395ed3302..e91e42c822 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -1,6 +1,5 @@
 # Build working directories
 tools/OpenROAD/build/
-tools/kepler-formal/build/
 # Local Bazel outputs; the image builds its own.
 etc/kepler-formal/bazel-*
 etc/kepler-formal/MODULE.bazel.lock
diff --git a/.gitmodules b/.gitmodules
index 20440a806e..bcda953424 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -4,6 +4,3 @@
 [submodule "tools/OpenROAD"]
 	path = tools/OpenROAD
 	url = ../OpenROAD.git
-[submodule "tools/kepler-formal"]
-	path = tools/kepler-formal
-	url = https://github.com/keplertech/kepler-formal
diff --git a/etc/DockerTag.sh b/etc/DockerTag.sh
index 5a4763da8e..2f10d8d81f 100755
--- a/etc/DockerTag.sh
+++ b/etc/DockerTag.sh
@@ -27,9 +27,9 @@ elif [[ "$@" == "-tools" ]]; then
         cat ./build_openroad.sh ./dev_env.sh ./etc/setup_compiler_wrappers.sh
         cat "${ignore_file}"
         # Drop the trailing describe output, which depends on fetched tags.
-        git submodule status tools/yosys tools/kepler-formal | awk '{print $1, $2}'
+        git submodule status tools/yosys | awk '{print $1, $2}'
         git ls-tree HEAD tools/ | grep -v -e 'tools/OpenROAD$' -e 'tools/AutoTuner$' \
-            -e 'tools/yosys$' -e 'tools/kepler-formal$'
+            -e 'tools/yosys$'
         # The kepler-formal version and the Bazel settings that install it.
         git ls-tree -r HEAD etc/kepler-formal
     } | sha256sum | awk '{print substr($1, 1, 6)}'
diff --git a/tools/kepler-formal b/tools/kepler-formal
deleted file mode 160000
index f70c2e3859..0000000000
--- a/tools/kepler-formal
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit f70c2e38592d704c8cccf68433b091e82c8118f0

From 2aa8f0a39cceea483f84889c229eb86f98b93a49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Sun, 25 Oct 2026 07:09:38 +0100
Subject: [PATCH 05/13] DependencyInstaller: drop the packages only
 kepler-formal needed
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

kepler-formal no longer builds against host packages: capnproto and
TBB on Ubuntu, EL and Homebrew, the oneTBB source build on EL8 and
gcc-toolset-13 on EL8 go.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 etc/DependencyInstaller.sh | 52 ++++----------------------------------
 1 file changed, 5 insertions(+), 47 deletions(-)

diff --git a/etc/DependencyInstaller.sh b/etc/DependencyInstaller.sh
index dc3cb17cb3..f09e285369 100755
--- a/etc/DependencyInstaller.sh
+++ b/etc/DependencyInstaller.sh
@@ -26,7 +26,7 @@ _versionCompare() {
     test $a "$2" $b
 }
 
-# Yosys and kepler-formal are built with CMake. Yosys needs CMake >= 3.28,
+# Yosys is built with CMake and needs CMake >= 3.28,
 # newer than Ubuntu 22.04 ships, so fetch a release from Kitware when the
 # one on PATH is too old.
 cmakeMinVersion=3.28
@@ -108,36 +108,6 @@ _installBison() {
     rm -rf "${workDir}"
 }
 
-# kepler-formal needs oneTBB and its CMake package. EL8 ships TBB 2018, which
-# has neither, so build oneTBB there. Build it static, because the
-# kepler-formal RPATH does not include the prefix.
-tbbVersion=2021.13.0
-tbbChecksum=3ad5dd08954b39d113dc5b3f8a8dc6dc1fd5250032b7c491eb07aed5c94133e1
-
-_installTbb() {
-    local prefix=${PREFIX:-"/usr/local"}
-    if compgen -G "${prefix}/lib*/cmake/TBB/TBBConfig.cmake" > /dev/null; then
-        echo "oneTBB found in ${prefix}, skipping install"
-        return
-    fi
-    local tarball="oneTBB-${tbbVersion}.tar.gz"
-    local workDir
-    workDir=$(mktemp -d)
-    (
-        # _installCmake may have put CMake in a prefix that is not on PATH.
-        export PATH="${prefix}/bin:${PATH}"
-        cd "${workDir}"
-        wget -q -O "${tarball}" "https://github.com/uxlfoundation/oneTBB/archive/refs/tags/v${tbbVersion}.tar.gz"
-        sha256sum -c <(echo "${tbbChecksum}  ${tarball}")
-        tar xzf "${tarball}"
-        cmake -S "oneTBB-${tbbVersion}" -B build -DCMAKE_BUILD_TYPE=Release \
-            -DTBB_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DCMAKE_INSTALL_PREFIX="${prefix}"
-        cmake --build build -j "${numThreads}"
-        cmake --install build
-    )
-    rm -rf "${workDir}"
-}
-
 _installORDependencies() {
     if [[ ${YOSYS_VER} == "" ]]; then
         YOSYS_VER=v$(grep 'yosys_ver =' tools/yosys/docs/source/conf.py | awk -F'"' '{print $2}')
@@ -232,14 +202,12 @@ _install_EL8_EL9_Packages() {
 
     # EL8 and EL9 use `dnf`, instead of `yum`
     dnf -y update
-    # EPEL has tcl-tclreadline and capnproto.
+    # EPEL has tcl-tclreadline.
     dnf -y install "https://dl.fedoraproject.org/pub/epel/epel-release-latest-${elVersion}.noarch.rpm"
-    # The rest builds Yosys and kepler-formal.
+    # The rest builds Yosys.
     dnf -y install \
         bison \
         boost-devel \
-        capnproto \
-        capnproto-devel \
         findutils \
         flex \
         gcc \
@@ -260,7 +228,7 @@ _install_EL8_EL9_Packages() {
         wget \
         zlib-devel
 
-    # kepler-formal and the pip lock files need Python 3.10 or newer, which
+    # The pip lock files need Python 3.10 or newer, which
     # is newer than the EL8 and EL9 defaults.
     dnf -y install python3.12 python3.12-devel python3.12-pip
     update-alternatives --install /usr/bin/python3 python3 "$(command -v python3.12)" 50
@@ -272,13 +240,9 @@ _install_EL8_EL9_Packages() {
             readline-devel \
             tcl-tclreadline \
             tcl-tclreadline-devel
-        # The default GCC 8 is too old for kepler-formal.
-        dnf -y install gcc-toolset-13
     fi
 
     if [[ "${elVersion}" == "9" ]]; then
-        # EL8 builds oneTBB instead, in -common.
-        dnf -y install tbb-devel
         dnf -y install \
             https://mirror.stream.centos.org/9-stream/AppStream/x86_64/os/Packages/readline-devel-8.1-4.el9.x86_64.rpm
     fi
@@ -345,13 +309,11 @@ _installUbuntuPackages() {
         bison \
         build-essential \
         ca-certificates \
-        capnproto \
         curl \
         flex \
         git \
         help2man \
         libboost-iostreams-dev \
-        libcapnp-dev \
         libffi-dev \
         libfl-dev \
         libfl2 \
@@ -364,7 +326,6 @@ _installUbuntuPackages() {
         libqt5svg5-dev \
         libqt5xmlpatterns5-dev \
         libreadline-dev \
-        libtbb-dev \
         libz-dev \
         perl \
         pkg-config \
@@ -467,7 +428,7 @@ _installUbuntuPackages() {
 
 _installDarwinPackages() {
     brew install libffi tcl-tk ruby
-    brew install python libomp doxygen capnp tbb bison flex boost spdlog zlib cmake
+    brew install python libomp doxygen bison flex boost spdlog zlib cmake
     brew link --force libomp
     brew install --cask klayout
     brew install docker docker-buildx
@@ -697,9 +658,6 @@ case "${os}" in
         if [[ "${option}" == "common" || "${option}" == "all" ]]; then
             _installCmake
             _installBison
-            if [[ "${elVersion}" == "8" ]]; then
-                _installTbb
-            fi
             _installPipCommon
         fi
         ;;

From 24b3a01a896b6e9f92c71fd38d02ea5066f4d00d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Wed, 4 Nov 2026 11:03:03 +0100
Subject: [PATCH 06/13] etc/kepler-formal: say why the C++ standard is set here
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 etc/kepler-formal/.bazelrc | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/etc/kepler-formal/.bazelrc b/etc/kepler-formal/.bazelrc
index bfb1b9cd74..c4d3616468 100644
--- a/etc/kepler-formal/.bazelrc
+++ b/etc/kepler-formal/.bazelrc
@@ -1,5 +1,8 @@
 common --registry=https://bcr.bazel.build/
 
+# kepler-formal and naja do not set the C++ standard on their targets,
+# so the build sets it, as their registry presubmits do. OpenROAD
+# requires C++20 too.
 build --cxxopt=-std=c++20
 build --host_cxxopt=-std=c++20
 build -c opt

From 65fab0f5b61f439b03f10d9a104a3db0f3d050a2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Wed, 4 Nov 2026 11:03:10 +0100
Subject: [PATCH 07/13] etc/kepler-formal: take kepler-formal from the registry
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

kepler-formal 0.5.0-20261026-a64adfaf is on the Bazel Central Registry
and has the //:install target, so the git_override on a fork goes.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 etc/kepler-formal/MODULE.bazel | 11 +----------
 etc/kepler-formal/README.md    |  6 +-----
 2 files changed, 2 insertions(+), 15 deletions(-)

diff --git a/etc/kepler-formal/MODULE.bazel b/etc/kepler-formal/MODULE.bazel
index 975f111008..6ec612ce23 100644
--- a/etc/kepler-formal/MODULE.bazel
+++ b/etc/kepler-formal/MODULE.bazel
@@ -7,16 +7,7 @@ kepler-formal into tools/install/kepler-formal. See README.md.
 module(name = "orfs-kepler-formal")
 
 # To bump kepler-formal, change this version.
-bazel_dep(name = "kepler-formal", version = "0.5.0-20261020-0be91596")
-
-# TODO(keplertech/kepler-formal#292): delete this override once a
-# kepler-formal version with the //:install target is on the registry,
-# and move the version above to it.
-git_override(
-    module_name = "kepler-formal",
-    commit = "99d66cac88978312853a10b82657781f8e99d843",
-    remote = "https://github.com/oharboe/kepler-formal.git",
-)
+bazel_dep(name = "kepler-formal", version = "0.5.0-20261026-a64adfaf")
 
 # kepler-formal builds with a downloaded clang. It registers that
 # toolchain for its own builds only, so a module that depends on it
diff --git a/etc/kepler-formal/README.md b/etc/kepler-formal/README.md
index 9b7495f429..ad2a477fb5 100644
--- a/etc/kepler-formal/README.md
+++ b/etc/kepler-formal/README.md
@@ -31,9 +31,5 @@ URL, the checksum and the build file of each version:
 
 ## What goes away as upstream merges
 
-1. When a registry version of kepler-formal has the install target
-   (keplertech/kepler-formal#292, after
-   bazelbuild/bazel-central-registry#11201): delete the `git_override` in
-   `MODULE.bazel` and move the version to it.
-2. When kepler-formal registers its compiler for modules that depend on
+1. When kepler-formal registers its compiler for modules that depend on
    it: delete the toolchain lines in `MODULE.bazel`.

From d3d8600991040556e119131fb0dd884f7a486f76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Wed, 4 Nov 2026 11:03:16 +0100
Subject: [PATCH 08/13] etc/kepler-formal: the compiler lines stay; llvm 0.8.26
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

kepler-formal keeps its clang toolchain a dev_dependency on purpose, so
a module that depends on it registers the toolchain itself; the README
no longer says these lines go away. llvm moves to 0.8.26, the version
kepler-formal builds with.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 etc/kepler-formal/MODULE.bazel | 7 ++++---
 etc/kepler-formal/README.md    | 5 -----
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/etc/kepler-formal/MODULE.bazel b/etc/kepler-formal/MODULE.bazel
index 6ec612ce23..44c36ccc0d 100644
--- a/etc/kepler-formal/MODULE.bazel
+++ b/etc/kepler-formal/MODULE.bazel
@@ -10,9 +10,10 @@ module(name = "orfs-kepler-formal")
 bazel_dep(name = "kepler-formal", version = "0.5.0-20261026-a64adfaf")
 
 # kepler-formal builds with a downloaded clang. It registers that
-# toolchain for its own builds only, so a module that depends on it
-# registers it too. Elsewhere the host compiler is used.
-bazel_dep(name = "llvm", version = "0.8.24")
+# toolchain for its own builds only, a dev_dependency by design, so a
+# module that depends on it registers it too, at the same version.
+# Elsewhere the host compiler is used.
+bazel_dep(name = "llvm", version = "0.8.26")
 
 llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain")
 use_repo(llvm_toolchains, "llvm_toolchains")
diff --git a/etc/kepler-formal/README.md b/etc/kepler-formal/README.md
index ad2a477fb5..a16ec0ea48 100644
--- a/etc/kepler-formal/README.md
+++ b/etc/kepler-formal/README.md
@@ -28,8 +28,3 @@ URL, the checksum and the build file of each version:
 | `gcc-toolset-13` on EL8, because GCC 8 is too old | A pinned clang is downloaded on x86-64 Linux; elsewhere the host compiler is used |
 | `tools/kepler-formal` and the submodules inside it | The version in `MODULE.bazel`; sources are checked against their checksums and cached in `~/.cache/bazel` |
 | An RPATH that points at the install's `lib/` | The binary finds its libraries next to itself, in `bin/kepler-formal.runfiles/` |
-
-## What goes away as upstream merges
-
-1. When kepler-formal registers its compiler for modules that depend on
-   it: delete the toolchain lines in `MODULE.bazel`.

From 6d431edc26e653dd0b3a9db50861516f01f646ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Sun, 8 Nov 2026 07:57:38 +0100
Subject: [PATCH 09/13] etc/kepler-formal: kepler-formal 1.0.0; clang on x86-64
 Linux only
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

kepler-formal 1.0.0-20261105-6870bd1a is on the Bazel Central Registry.
Its .github/consumer-test registers the downloaded clang for x86-64
Linux only, so this module does the same and other platforms use the
host compiler, as the README says. The dynamic_mode comment gives
kepler-formal's reason for the flag.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 etc/kepler-formal/.bazelrc     |  3 ++-
 etc/kepler-formal/MODULE.bazel | 19 ++++++++++++++-----
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/etc/kepler-formal/.bazelrc b/etc/kepler-formal/.bazelrc
index c4d3616468..bb69887287 100644
--- a/etc/kepler-formal/.bazelrc
+++ b/etc/kepler-formal/.bazelrc
@@ -7,6 +7,7 @@ build --cxxopt=-std=c++20
 build --host_cxxopt=-std=c++20
 build -c opt
 
-# As kepler-formal's own .bazelrc.
+# As kepler-formal's own .bazelrc: the downloaded clang toolchain must
+# win resolution on Linux.
 common --enable_platform_specific_config
 build:linux --dynamic_mode=off
diff --git a/etc/kepler-formal/MODULE.bazel b/etc/kepler-formal/MODULE.bazel
index 44c36ccc0d..607087bc21 100644
--- a/etc/kepler-formal/MODULE.bazel
+++ b/etc/kepler-formal/MODULE.bazel
@@ -7,15 +7,24 @@ kepler-formal into tools/install/kepler-formal. See README.md.
 module(name = "orfs-kepler-formal")
 
 # To bump kepler-formal, change this version.
-bazel_dep(name = "kepler-formal", version = "0.5.0-20261026-a64adfaf")
+bazel_dep(name = "kepler-formal", version = "1.0.0-20261105-6870bd1a")
 
-# kepler-formal builds with a downloaded clang. It registers that
-# toolchain for its own builds only, a dev_dependency by design, so a
-# module that depends on it registers it too, at the same version.
-# Elsewhere the host compiler is used.
+# kepler-formal builds with a downloaded clang on x86-64 Linux. It
+# registers that toolchain for its own builds only, a dev_dependency by
+# design, so a module that depends on it registers it too, at the same
+# version, as kepler-formal's .github/consumer-test does. Elsewhere the
+# host compiler is used.
 bazel_dep(name = "llvm", version = "0.8.26")
 
 llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain")
+llvm_toolchains.exec(
+    arch = "x86_64",
+    os = "linux",
+)
+llvm_toolchains.target(
+    arch = "x86_64",
+    os = "linux",
+)
 use_repo(llvm_toolchains, "llvm_toolchains")
 
 register_toolchains("@llvm_toolchains//:all")

From 138705343e34bae5622d79de9ad1e4f5736f5c3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Mon, 9 Nov 2026 19:56:56 +0100
Subject: [PATCH 10/13] EL8: keep gcc-toolset-13 for Yosys
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Yosys is still built with CMake before kepler-formal, and the pinned
Yosys sets CMAKE_CXX_STANDARD 20, which the EL8 default GCC 8 cannot
compile. The OpenROAD installer pinned here is Bazel-only and installs
no host compiler, and the clang that kepler-formal downloads does not
apply to the Yosys build.

Keep installing gcc-toolset-13 on EL8 and keep sourcing it in
build_openroad.sh, where it stays active for the kepler-formal install:
on aarch64 no downloaded clang is registered and the host compiler is
used.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 build_openroad.sh           | 8 ++++++++
 etc/DependencyInstaller.sh  | 2 ++
 etc/kepler-formal/README.md | 2 +-
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/build_openroad.sh b/build_openroad.sh
index 580a6f9ce9..2b9111af25 100755
--- a/build_openroad.sh
+++ b/build_openroad.sh
@@ -385,6 +385,14 @@ __local_build()
                 source /opt/rh/devtoolset-8/enable
                 set -u
         fi
+        # EL8: the default GCC 8 is too old for Yosys, which needs C++20.
+        # It stays active for kepler-formal, which uses the host compiler
+        # where no downloaded clang is registered (aarch64).
+        if [[ -f "/opt/rh/gcc-toolset-13/enable" ]]; then
+                set +u
+                source /opt/rh/gcc-toolset-13/enable
+                set -u
+        fi
 
         if [ -z "${SKIP_OPENROAD+x}" ]; then
                 echo "[INFO FLW-0018] Compiling OpenROAD."
diff --git a/etc/DependencyInstaller.sh b/etc/DependencyInstaller.sh
index bad223b245..309c7dbf81 100755
--- a/etc/DependencyInstaller.sh
+++ b/etc/DependencyInstaller.sh
@@ -244,6 +244,8 @@ _install_EL8_EL9_Packages() {
             readline-devel \
             tcl-tclreadline \
             tcl-tclreadline-devel
+        # The default GCC 8 is too old for Yosys, which needs C++20.
+        dnf -y install gcc-toolset-13
     fi
 
     if [[ "${elVersion}" == "9" ]]; then
diff --git a/etc/kepler-formal/README.md b/etc/kepler-formal/README.md
index a16ec0ea48..8a5e4b736c 100644
--- a/etc/kepler-formal/README.md
+++ b/etc/kepler-formal/README.md
@@ -25,6 +25,6 @@ URL, the checksum and the build file of each version:
 | --- | --- |
 | oneTBB and capnproto from the OS, or built from a pinned tarball | `bazel_dep` versions in kepler-formal's `MODULE.bazel` |
 | A pinned CMake when the OS's is too old | bazelisk runs the Bazel named in `.bazelversion` |
-| `gcc-toolset-13` on EL8, because GCC 8 is too old | A pinned clang is downloaded on x86-64 Linux; elsewhere the host compiler is used |
+| `gcc-toolset-13` on EL8, because GCC 8 is too old | A pinned clang is downloaded on x86-64 Linux; elsewhere the host compiler is used, `gcc-toolset-13` on EL8, which Yosys still needs |
 | `tools/kepler-formal` and the submodules inside it | The version in `MODULE.bazel`; sources are checked against their checksums and cached in `~/.cache/bazel` |
 | An RPATH that points at the install's `lib/` | The binary finds its libraries next to itself, in `bin/kepler-formal.runfiles/` |

From 1da6017f5f40a45996d51b2428da243bff2bfcb6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Mon, 9 Nov 2026 19:57:05 +0100
Subject: [PATCH 11/13] .dockerignore: exclude tools/kepler-formal/
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A checkout made before the submodule was removed keeps the old
tools/kepler-formal tree. It would enter the Docker build context and
the license collector, which searches tools/.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 .dockerignore | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.dockerignore b/.dockerignore
index e91e42c822..75e99b1d85 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -1,5 +1,8 @@
 # Build working directories
 tools/OpenROAD/build/
+# A checkout from before kepler-formal moved to etc/kepler-formal keeps
+# the old submodule tree; keep it out of the image and its licenses.
+tools/kepler-formal/
 # Local Bazel outputs; the image builds its own.
 etc/kepler-formal/bazel-*
 etc/kepler-formal/MODULE.bazel.lock

From 9f240ea9b08b86feb6f044cf153b6b7418a80094 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Mon, 9 Nov 2026 19:58:46 +0100
Subject: [PATCH 12/13] etc/kepler-formal/.bazelrc: say what dynamic_mode=off
 does
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The comment said the downloaded clang must win resolution on Linux, but
the line below only links statically. Clang is chosen by
register_toolchains in MODULE.bazel, on x86-64 Linux only.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 etc/kepler-formal/.bazelrc | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/etc/kepler-formal/.bazelrc b/etc/kepler-formal/.bazelrc
index bb69887287..9b9d949212 100644
--- a/etc/kepler-formal/.bazelrc
+++ b/etc/kepler-formal/.bazelrc
@@ -7,7 +7,8 @@ build --cxxopt=-std=c++20
 build --host_cxxopt=-std=c++20
 build -c opt
 
-# As kepler-formal's own .bazelrc: the downloaded clang toolchain must
-# win resolution on Linux.
+# As kepler-formal's own .bazelrc: link statically on Linux. The clang
+# toolchain is chosen by register_toolchains in MODULE.bazel, on x86-64
+# Linux only.
 common --enable_platform_specific_config
 build:linux --dynamic_mode=off

From 225ee8820e6775a4119bae898d9e8eb214cc39cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98yvind=20Harboe?= <oyvind.harboe@zylin.com>
Date: Mon, 9 Nov 2026 20:02:14 +0100
Subject: [PATCH 13/13] kepler-formal: install the dependency license notices
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

kepler-formal's //:install ships only its own LICENSE.rst and
LICENSES/, while the binary links naja, yaml-cpp, spdlog, kissat and
more, statically links libc++, and carries an embedded Python in its
runfiles. The Docker license collector searches tools/ and cannot find
notices in the Bazel cache.

etc/kepler-formal/install_licenses.sh, run by build_openroad.sh after
the install, takes the repositories cquery finds in the binary's target
configuration and copies their license notices to
share/kepler-formal/licenses/<repository>/ under the same prefix. Build
tools that run in the exec configuration are left out. It fails if it
finds none.

On x86-64 Linux it installs the notices of 40 modules, 1.1 MB.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>
---
 build_openroad.sh                     |  3 +-
 etc/kepler-formal/README.md           |  9 +++++
 etc/kepler-formal/install_licenses.sh | 54 +++++++++++++++++++++++++++
 3 files changed, 65 insertions(+), 1 deletion(-)
 create mode 100755 etc/kepler-formal/install_licenses.sh

diff --git a/build_openroad.sh b/build_openroad.sh
index 2b9111af25..3ccfd38842 100755
--- a/build_openroad.sh
+++ b/build_openroad.sh
@@ -437,7 +437,8 @@ __local_build()
                 KEPLER_PREFIX="$(pwd)/${KEPLER_PREFIX}"
         fi
         (cd "${DIR}/etc/kepler-formal" && \
-                ${NICE} bazelisk run --jobs="${PROC}" //:install -- "${KEPLER_PREFIX}")
+                ${NICE} bazelisk run --jobs="${PROC}" //:install -- "${KEPLER_PREFIX}" && \
+                ./install_licenses.sh "${KEPLER_PREFIX}")
 
         if [ ${WITH_VERIFIC} -eq 1 ]; then
                 echo "[INFO FLW-0032] Cleaning up Verific components."
diff --git a/etc/kepler-formal/README.md b/etc/kepler-formal/README.md
index 8a5e4b736c..62e16601aa 100644
--- a/etc/kepler-formal/README.md
+++ b/etc/kepler-formal/README.md
@@ -13,6 +13,15 @@ bazelisk run //:install -- "$(pwd)/../../tools/install/kepler-formal"
 ORFS is not a Bazel project. This folder only pins kepler-formal; the
 install is kepler-formal's own `//:install` target.
 
+That target installs only kepler-formal's own license. `build_openroad.sh`
+then runs `install_licenses.sh` with the same prefix, which copies the
+license notices of every module linked into the binary or shipped in its
+runfiles to `share/kepler-formal/licenses/<module>/`:
+
+```shell
+./install_licenses.sh "$(pwd)/../../tools/install/kepler-formal"
+```
+
 ## How this maps to `DependencyInstaller.sh`
 
 `DependencyInstaller.sh` downloads a pinned CMake from Kitware when the
diff --git a/etc/kepler-formal/install_licenses.sh b/etc/kepler-formal/install_licenses.sh
new file mode 100755
index 0000000000..d41774b925
--- /dev/null
+++ b/etc/kepler-formal/install_licenses.sh
@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+# Usage: install_licenses.sh <prefix>
+#
+# Copies the license notices of every module that goes into the
+# kepler-formal binary and its runfiles (naja, yaml-cpp, spdlog, kissat,
+# the embedded Python, the statically linked libc++, ...) into
+# <prefix>/share/kepler-formal/licenses/<repository>/. kepler-formal's
+# //:install ships only its own LICENSE.rst and LICENSES/.
+#
+# The modules are the repositories cquery finds in the binary's target
+# configuration; build tools such as bison run in the exec configuration
+# and are left out. Run it after `bazelisk run //:install`, from this
+# folder, so that the repositories are fetched.
+set -euo pipefail
+
+if [[ $# -ne 1 ]]; then
+    echo "Usage: $0 <prefix>" >&2
+    exit 1
+fi
+dest="$(cd "$1" && pwd)/share/kepler-formal/licenses"
+binary=@kepler-formal//src/bin:kepler-formal
+
+cd "$(dirname "$0")"
+external="$(bazelisk info output_base)/external"
+config="$(bazelisk cquery "${binary}" | awk '{print $NF}')"
+repos="$(bazelisk cquery --consistent_labels "deps(${binary})" \
+    | awk -v c="${config}" '$NF == c' \
+    | sed -n 's|^@@\([^/]*\)//.*|\1|p' | sort -u)"
+
+rm -rf "${dest}"
+count=0
+for repo in ${repos}; do
+    [[ -n "${repo}" ]] || continue
+    # Some modules unpack into a subdirectory (zlib-1.3.2/, slang-12.0/),
+    # and the llvm-project one keeps libc++'s notice in libcxx/. The
+    # embedded Python keeps its own in lib/python3.X/.
+    files="$(cd "${external}/${repo}" && find . -maxdepth 3 \
+        \( \( -iname 'LICENSE*' -o -iname 'LICENCE*' -o -iname 'COPYING*' \
+              -o -iname 'NOTICE*' -o -iname 'COPYRIGHT*' \) \
+           \( -path './*' -a ! -path './*/*/*' \
+              -o -path './lib/python*/LICENSE.txt' \) \) \
+        -print -prune)"
+    [[ -n "${files}" ]] || continue
+    mkdir -p "${dest}/${repo}"
+    while IFS= read -r f; do
+        (cd "${external}/${repo}" && cp -rL --parents "${f}" "${dest}/${repo}/")
+    done <<< "${files}"
+    count=$((count + 1))
+done
+if [[ ${count} -eq 0 ]]; then
+    echo "[ERROR] no license notices found for ${binary} in ${external}" >&2
+    exit 1
+fi
+echo "Installed the license notices of ${count} modules in ${dest}"