sync

.bazelrc

@@ -2,11 +2,13 @@ common --enable_platform_specific_config
 
 build --cxxopt=-std=c++20
 build --host_cxxopt=-std=c++20
+build --workspace_status_command=tools/workspace_status.sh
 
 # Never fall back to autodetecting /usr/bin/gcc on Linux — the hermetic
 # toolchain (hermetic-llvm) must win resolution. macOS still uses the
 # host toolchain, so the guard is Linux-scoped.
 common:linux --repo_env=BAZEL_DO_NOT_DETECT_CPP_TOOLCHAIN=1
+build:linux --dynamic_mode=off
 
 # Force C11 for host tools to work around rules_foreign_cc pkg-config
 # bootstrap failure: bundled glib uses 'bool' as a struct field name,

.github/workflows/c-cpp.yml

@@ -42,9 +42,17 @@ jobs:
     - name: Build
       run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}}
 
+    - name: Generate Naja IF test inputs with the local Naja checkout
+      working-directory: ${{github.workspace}}/examples/tinyrocket
+      run: |
+        python3 -m pip install --upgrade "scikit-build-core>=0.11.3,<0.12"
+        CMAKE_ARGS="-DPREGENERATED_PARSER_SOURCES=OFF" \
+          python3 -m pip install --no-build-isolation "${{github.workspace}}/thirdparty/naja"
+        python3 to_naja_if.py
+        python3 edit.py
+
     - name: Test
       working-directory: ${{github.workspace}}/build
       env:
         PYTHONMALLOC: malloc
       run: ctest -VV -E ".*[p|P]ython.*" -C ${{ env.BUILD_TYPE }}
-

.github/workflows/coverage.yml

@@ -50,6 +50,19 @@ jobs:
         CC:   clang
         CXX:  clang++
 
+    - name: Generate Naja IF test inputs with the local Naja checkout
+      working-directory: ${{github.workspace}}/examples/tinyrocket
+      env:
+        GIT_CONFIG_COUNT: "1"
+        GIT_CONFIG_KEY_0: core.abbrev
+        GIT_CONFIG_VALUE_0: "7"
+      run: |
+        python3 -m pip install --upgrade "scikit-build-core>=0.11.3,<0.12"
+        CMAKE_ARGS="-DPREGENERATED_PARSER_SOURCES=OFF" \
+          python3 -m pip install --no-build-isolation "${{github.workspace}}/thirdparty/naja"
+        python3 to_naja_if.py
+        python3 edit.py
+
     - name: Test
       working-directory: ${{github.workspace}}/build
       env:

.github/workflows/cva6imc.yml

@@ -66,6 +66,7 @@ jobs:
         export HPDCACHE_DIR="$PWD/core/cache_subsystem/hpdcache"
         export TARGET_CFG="cv64a6_imafdc_sv39"
         export LD_LIBRARY_PATH="${{github.workspace}}/stage/lib:${LD_LIBRARY_PATH}"
+        set +e
         "${{github.workspace}}/stage/bin/kepler-formal" -systemverilog \
           --compact \
           -v sec \
@@ -74,4 +75,12 @@ jobs:
           --sv_design1_flist "$PWD/core/Flist.cva6" \
           --sv_design1_top cva6 \
           --sv_design2_flist "$PWD/core/Flist.cva6" \
-          --sv_design2_top cva6
+          --sv_design2_top cva6 2>&1 | tee "${RUNNER_TEMP}/cva6-imc.log"
+        status=${PIPESTATUS[0]}
+        set -e
+        # Positive self-SEC accepts a proved or explicitly partial verdict.
+        if [[ "${status}" -eq 1 ]] &&
+            grep -q "SEC partially proved equivalence" "${RUNNER_TEMP}/cva6-imc.log"; then
+          exit 0
+        fi
+        exit "${status}"

.github/workflows/cva6ki.yml

@@ -66,6 +66,7 @@ jobs:
         export HPDCACHE_DIR="$PWD/core/cache_subsystem/hpdcache"
         export TARGET_CFG="cv64a6_imafdc_sv39"
         export LD_LIBRARY_PATH="${{github.workspace}}/stage/lib:${LD_LIBRARY_PATH}"
+        set +e
         "${{github.workspace}}/stage/bin/kepler-formal" -systemverilog \
           --compact \
           -v sec \
@@ -74,4 +75,12 @@ jobs:
           --sv_design1_flist "$PWD/core/Flist.cva6" \
           --sv_design1_top cva6 \
           --sv_design2_flist "$PWD/core/Flist.cva6" \
-          --sv_design2_top cva6
+          --sv_design2_top cva6 2>&1 | tee "${RUNNER_TEMP}/cva6-ki.log"
+        status=${PIPESTATUS[0]}
+        set -e
+        # Positive self-SEC accepts a proved or explicitly partial verdict.
+        if [[ "${status}" -eq 1 ]] &&
+            grep -q "SEC partially proved equivalence" "${RUNNER_TEMP}/cva6-ki.log"; then
+          exit 0
+        fi
+        exit "${status}"

.github/workflows/cva6pdr.yml

@@ -66,6 +66,7 @@ jobs:
         export HPDCACHE_DIR="$PWD/core/cache_subsystem/hpdcache"
         export TARGET_CFG="cv64a6_imafdc_sv39"
         export LD_LIBRARY_PATH="${{github.workspace}}/stage/lib:${LD_LIBRARY_PATH}"
+        set +e
         "${{github.workspace}}/stage/bin/kepler-formal" -systemverilog \
           --compact \
           -v sec \
@@ -74,4 +75,12 @@ jobs:
           --sv_design1_flist "$PWD/core/Flist.cva6" \
           --sv_design1_top cva6 \
           --sv_design2_flist "$PWD/core/Flist.cva6" \
-          --sv_design2_top cva6
+          --sv_design2_top cva6 2>&1 | tee "${RUNNER_TEMP}/cva6-pdr.log"
+        status=${PIPESTATUS[0]}
+        set -e
+        # Positive self-SEC accepts a proved or explicitly partial verdict.
+        if [[ "${status}" -eq 1 ]] &&
+            grep -q "SEC partially proved equivalence" "${RUNNER_TEMP}/cva6-pdr.log"; then
+          exit 0
+        fi
+        exit "${status}"

.github/workflows/macOS.yml

@@ -40,6 +40,16 @@ jobs:
       # Build your program with the given configuration
       run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}}
 
+    - name: Generate Naja IF test inputs with the local Naja checkout
+      working-directory: ${{github.workspace}}/examples/tinyrocket
+      run: |
+        python3 -m venv "${RUNNER_TEMP}/najaeda-venv"
+        source "${RUNNER_TEMP}/najaeda-venv/bin/activate"
+        CMAKE_ARGS="-DPREGENERATED_PARSER_SOURCES=OFF" \
+          python3 -m pip install "${{github.workspace}}/thirdparty/naja"
+        python3 to_naja_if.py
+        python3 edit.py
+
     - name: Test
       working-directory: ${{github.workspace}}/build
       env:

.github/workflows/mcp.yml

@@ -0,0 +1,24 @@
+# Copyright 2026 keplertech.io
+# SPDX-License-Identifier: Apache-2.0
+
+name: mcp
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  test:
+    strategy:
+      matrix:
+        python-version: ["3.10", "3.14"]
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python-version }}
+      - name: Install optional MCP add-on
+        run: python -m pip install ./mcp
+      - name: Test MCP add-on
+        run: python -m unittest discover -s mcp/tests -v

.github/workflows/nix-prebuilt.yml

@@ -0,0 +1,75 @@
+# Copyright 2026 keplertech.io
+# SPDX-License-Identifier: Apache-2.0
+
+name: nix-prebuilt
+
+on:
+  workflow_dispatch:
+    inputs:
+      ref:
+        description: Published branch or tag to install (must already be cached)
+        type: string
+        required: true
+        default: main
+      revision:
+        description: Optional published commit SHA (defaults to the current ref)
+        type: string
+        required: false
+        default: ''
+  workflow_call:
+    inputs:
+      ref:
+        type: string
+        required: true
+      revision:
+        type: string
+        required: false
+        default: ''
+
+permissions:
+  contents: read
+
+jobs:
+  install:
+    name: install ${{ matrix.system }}
+    timeout-minutes: 20
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - os: ubuntu-24.04
+            system: x86_64-linux
+          - os: macos-latest
+            system: aarch64-darwin
+    runs-on: ${{ matrix.os }}
+    steps:
+      # These are fresh runners, not the jobs that built/published the package.
+      # Only the smoke-test scripts are needed from the checkout.
+      - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5.1.0
+        with:
+          persist-credentials: false
+      - uses: cachix/install-nix-action@8aa03977d8d733052d78f4e008a241fd1dbf36b3 # v31.10.6
+        with:
+          install_url: https://releases.nixos.org/nix/nix-2.35.1/install
+          enable_kvm: false
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+            max-jobs = 0
+            builders =
+            allow-import-from-derivation = false
+      - uses: cachix/cachix-action@38b082610b782e7e93e209c35fd730d399dee866 # v17
+        with:
+          name: keplertech
+          skipPush: true
+      - name: Install and test the public prebuilt CLI (no builds)
+        shell: bash
+        env:
+          INSTALL_REF: ${{ inputs.ref }}
+          PUBLISHED_SHA: ${{ inputs.revision }}
+        run: |
+          flake="git+https://github.com/keplertech/kepler-formal?ref=$INSTALL_REF"
+          if [[ -n "$PUBLISHED_SHA" ]]; then
+            # Pin the publication's exact revision even if its branch moves.
+            flake="$flake&rev=$PUBLISHED_SHA"
+          fi
+          bash nix/check-prebuilt.sh "$flake"

.github/workflows/nix.yml

@@ -0,0 +1,74 @@
+# Copyright 2026 keplertech.io
+# SPDX-License-Identifier: Apache-2.0
+
+name: nix
+
+on:
+  pull_request:
+  push:
+    branches: [main, nixOS]
+    tags: ['v*']
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  build-and-check:
+    name: ${{ matrix.system }}
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - os: ubuntu-24.04
+            system: x86_64-linux
+          - os: macos-latest
+            system: aarch64-darwin
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5.1.0
+        with:
+          submodules: recursive
+          persist-credentials: false
+      - uses: cachix/install-nix-action@8aa03977d8d733052d78f4e008a241fd1dbf36b3 # v31.10.6
+        with:
+          install_url: https://releases.nixos.org/nix/nix-2.35.1/install
+      - uses: cachix/cachix-action@38b082610b782e7e93e209c35fd730d399dee866 # v17
+        with:
+          name: keplertech
+          skipPush: true
+      - name: Check installed package
+        run: nix flake check --system ${{ matrix.system }} --print-build-logs --no-update-lock-file
+      - name: Build CLI package
+        run: nix build .#packages.${{ matrix.system }}.default --print-build-logs --no-update-lock-file
+      - name: Publish CLI package
+        if: github.repository == 'keplertech/kepler-formal' && github.event_name == 'workflow_dispatch'
+        env:
+          CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_AUTH_TOKEN }}
+          NIX_SYSTEM: ${{ matrix.system }}
+        run: |
+          : "${CACHIX_AUTH_TOKEN:?Set the CACHIX_AUTH_TOKEN repository secret}"
+          package_path=$(nix path-info ./result)
+          cachix push keplertech "$package_path"
+          cachix pin keplertech "kepler-formal-$NIX_SYSTEM" "$package_path" --keep-revisions 20
+      - name: Verify public cache download
+        if: github.repository == 'keplertech/kepler-formal' && github.event_name == 'workflow_dispatch'
+        run: |
+          package_path=$(nix path-info ./result)
+          nix path-info --store https://keplertech.cachix.org "$package_path" \
+            --option narinfo-cache-negative-ttl 0
+          verify_root=$(mktemp -d "$RUNNER_TEMP/cachix-verify.XXXXXX")
+          nix-store --store "$verify_root" --realise "$package_path" \
+            --max-jobs 0 --option builders '' \
+            --option substituters 'https://keplertech.cachix.org https://cache.nixos.org' \
+            --option extra-substituters '' --option narinfo-cache-negative-ttl 0
+
+  test-prebuilt-install:
+    # PR/push runs do not publish. After manual publication, verify real profile
+    # installation on fresh runners that cannot reuse the preceding build.
+    needs: build-and-check
+    if: github.repository == 'keplertech/kepler-formal' && github.event_name == 'workflow_dispatch'
+    uses: ./.github/workflows/nix-prebuilt.yml
+    with:
+      ref: ${{ github.ref_name }}
+      revision: ${{ github.sha }}