From f3fe83aa1ae362fce27a37558764f574b12a005d Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 14:33:47 -0400
Subject: [PATCH 1/7] ci: split lean-test into a cached build + parallel test
 matrix

Replace the single serial lean-test job with a `build` producer that
compiles Ix (and lints every target under --wfail) once and caches the
`.lake`, plus a two-suite `test` matrix that restores it:

- core: CLI + Aiur tests
- tc: Ix.Tc verification, the ~13-min Ix.Tc.Verify proof elaboration,
  and the production parity/scale run

The tc suite keeps its own `lake-tc-*` cache so the proof build persists
across commits (Lake's per-module traces guarantee a stale restore only
forces a rebuild, never a wrong olean); core restores the base build
read-only. This overlaps the proof elaboration with the core suite
instead of serializing it, and reuses it on runs that don't touch the
typechecker.

Required status checks change: `lean-test` is replaced by `Build Ix`,
`CLI and Aiur tests`, and `Ix.Tc verification and parity`.
---
 .github/workflows/ci.yml | 111 ++++++++++++++++++++++++++++++---------
 1 file changed, 86 insertions(+), 25 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d1f072b7..8ac870bd 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -26,8 +26,8 @@ jobs:
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       # Build only the compiler executable and its dependencies. In particular,
       # a failure in an unrelated Tests module must not prevent fixture
-      # publication. Disable the Lean cache because lean-test builds the same
-      # revision concurrently and the two jobs must not race to save one key.
+      # publication. Disable the Lean cache because the `build` job builds the
+      # same revision concurrently and the two jobs must not race to save one key.
       - uses: leanprover/lean-action@v1
         with:
           auto-config: false
@@ -47,7 +47,13 @@ jobs:
           if-no-files-found: error
           retention-days: 1
 
-  lean-test:
+  # Build Ix once — with the --wfail lint gate over every lib/exe target — and
+  # let lean-action cache the full `.lake` under its per-sha key. The parallel
+  # `test` matrix restores that exact build instead of each suite recompiling
+  # the base, and ignored.yml keeps restoring the same key. `test: false` keeps
+  # this job build-only; the suites run the tests.
+  build:
+    name: Build Ix
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7
@@ -55,44 +61,99 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail -v"
+          test: false
       # build-all lint driver compiles every lib/exe target with --wfail, so a
       # warning in any target (exes, benchmarks, Apps) — not just the default lib
-      # lean-action builds above — fails CI.
+      # lean-action builds above — fails CI. Building them here also populates
+      # the cache the test matrix restores.
       - name: Build all targets
         run: lake lint -- --wfail -v
-      - name: Check Ix.Tc verification sorry frontier
+      - name: Check codegen'd IxVM kernel is up to date
+        run: lake exe ix codegen --check
+      - name: Check Lean versions match for Ix and compiler bench
+        run: diff lean-toolchain Benchmarks/Compile/lean-toolchain
+
+  # Two parallel test suites over the base build the `build` job cached. Each
+  # restores `.lake` rather than recompiling Ix; lean-action just provisions the
+  # toolchain (no build/cache) and the suite's `lake test` steps run against the
+  # restored build. The tc suite's heavyweight secondary work — the ~13-min
+  # `Ix.Tc.Verify` proof elaboration and parity run — is what keeps the split
+  # worthwhile: it overlaps the core suite instead of serializing behind it.
+  test:
+    needs: build
+    name: ${{ matrix.name }}
+    runs-on: warp-ubuntu-latest-x64-16x
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - suite: core
+            name: CLI and Aiur tests
+          - suite: tc
+            name: Ix.Tc verification and parity
+    steps:
+      - uses: actions/checkout@v7
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      # Core restores the base build read-only (exact per-sha key the `build`
+      # job wrote, prefix fallback otherwise).
+      - if: matrix.suite == 'core'
+        uses: actions/cache/restore@v6
+        with:
+          path: .lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
+      # The tc suite keeps its own `lake-tc-…` cache so it can additionally
+      # persist the proof elaboration across commits: restore its latest prior
+      # build first, fall back to the base build, and save the proof-laden
+      # `.lake` at job end. Correctness is Lake's — a stale restore forces a
+      # rebuild via per-module traces, never a wrong olean.
+      - if: matrix.suite == 'tc'
+        uses: actions/cache@v6
+        with:
+          path: .lake
+          key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: |
+            lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - if: matrix.suite == 'core'
+        name: Test Ix CLI
+        run: lake test --wfail -- cli
+      - if: matrix.suite == 'core'
+        name: Aiur tests
+        run: lake test --wfail -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier
+      - if: matrix.suite == 'tc'
+        name: Check Ix.Tc verification sorry frontier
         run: perl .github/scripts/check_tc_verify_sorries.pl
-      - name: Check Ix.Tc exported theorem trust manifest
+      - if: matrix.suite == 'tc'
+        name: Check Ix.Tc exported theorem trust manifest
         run: lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Statements
-      - name: Build Ix.Tc formal verification
+      - if: matrix.suite == 'tc'
+        name: Build Ix.Tc formal verification
         run: lake build IxTcVerify
-      # The verification release claim includes executable adversarial and
-      # production-parity evidence.  Its exact pin/accelerator seed closure is
-      # deliberately separate from the much smaller zkVM smoke fixture. Doing
-      # this after lean-action avoids another Lean build/cache consumer and
-      # keeps lean-test independent of the zkVM artifact producer.
-      - name: Test Ix.Tc unit and adversarial fixtures
+      - if: matrix.suite == 'tc'
+        name: Test Ix.Tc unit and adversarial fixtures
         run: lake test --wfail -- tc-unit
-      - name: Compile Ix.Tc parity fixture
+      - if: matrix.suite == 'tc'
+        name: Compile Ix.Tc parity fixture
         run: >-
           lake exe ix compile Ix.lean
           --consts-file .github/fixtures/tc-parity-consts.txt
           --out tc-parity.ixe
-      - name: Test Ix.Tc production parity and scale
+      # The verification release claim includes executable adversarial and
+      # production-parity evidence. Its exact pin/accelerator seed closure is
+      # deliberately separate from the much smaller zkVM smoke fixture.
+      - if: matrix.suite == 'tc'
+        name: Test Ix.Tc production parity and scale
         run: >-
           lake test --wfail -- --ignored
           tc-pins tc-accel-diff tc-anon-diff tc-roundtrip tc-init
           tc-tutorial lean4lean
         env:
           IX_PINS_IXE: tc-parity.ixe
-      - name: Check codegen'd IxVM kernel is up to date
-        run: lake exe ix codegen --check
-      - name: Test Ix CLI
-        run: lake test --wfail -- cli
-      - name: Aiur tests
-        run: lake test --wfail -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier
-      - name: Check Lean versions match for Ix and compiler bench
-        run: diff lean-toolchain Benchmarks/Compile/lean-toolchain
 
   rust-test:
     runs-on: ubuntu-latest
@@ -128,8 +189,8 @@ jobs:
   # failures by design (dropped rows, OOM sentinels), so they never turn red
   # on a breakage. These jobs are the red-X signal: each builds its host, then
   # runs the guest in the VM over `nataddcomm.ixe` (a ~40-constant closure the
-  # dedicated zkvm-fixture job publishes). They run in parallel with lean-test
-  # and with each other after that narrow producer succeeds. Both hosts exit
+  # dedicated zkvm-fixture job publishes). They run in parallel with the Lean
+  # jobs and with each other after that narrow producer succeeds. Both hosts exit
   # non-zero when the kernel rejects a constant (sp1: EXIT_REJECTED; zisk:
   # `reject_failures`), so a guest that compiles but panics / faults / rejects
   # fails the job. SP1 execute is pure RISC-V emulation (no key). Zisk execute

From 4f2565214bc716444aee394f264d6bd5d5a4c724 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 14:53:12 -0400
Subject: [PATCH 2/7] ci: fold zkvm-fixture into the build job
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The zkvm-fixture job rebuilt `ix` from scratch just to compile the
~40-constant nataddcomm.ixe closure — duplicating the build job's `ix`
compile every run. Move the fixture compile + upload into `build`, and
point sp1-build/zisk-build at `needs: build`.

Tradeoff: the zkVM execution gates now gate on the full build (Ix +
all-targets lint) succeeding, not just `ix` compiling as before. Since
`needs` gates on job success regardless, that independence can't be kept
while keying the gates off `build`.
---
 .github/workflows/ci.yml | 59 ++++++++++++++--------------------------
 1 file changed, 21 insertions(+), 38 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8ac870bd..a0bca81f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -14,44 +14,14 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  # Produce the small real-program fixture consumed by both zkVM execution
-  # gates independently of the full Lean test job. A workflow artifact is the
-  # right synchronization primitive here: the file is unique to this run and
-  # must be available before either consumer starts.
-  zkvm-fixture:
-    name: zkVM execution fixture
-    runs-on: warp-ubuntu-latest-x64-16x
-    steps:
-      - uses: actions/checkout@v7
-      - uses: actions-rust-lang/setup-rust-toolchain@v1
-      # Build only the compiler executable and its dependencies. In particular,
-      # a failure in an unrelated Tests module must not prevent fixture
-      # publication. Disable the Lean cache because the `build` job builds the
-      # same revision concurrently and the two jobs must not race to save one key.
-      - uses: leanprover/lean-action@v1
-        with:
-          auto-config: false
-          build: true
-          build-args: "ix --wfail -v"
-          use-github-cache: false
-      # `Nat.add_comm`'s transitive-dependency closure (~40 kB, ~40 constants)
-      # is a real theorem, not an empty environment. `--consts` keeps this much
-      # smaller than the complete Init+Std environment used by benchmarks.
-      - name: Compile nataddcomm.ixe
-        run: lake exe ix compile Ix.lean --consts Nat.add_comm --out nataddcomm.ixe
-      - name: Upload nataddcomm.ixe
-        uses: actions/upload-artifact@v4
-        with:
-          name: nataddcomm-ixe
-          path: nataddcomm.ixe
-          if-no-files-found: error
-          retention-days: 1
-
   # Build Ix once — with the --wfail lint gate over every lib/exe target — and
   # let lean-action cache the full `.lake` under its per-sha key. The parallel
   # `test` matrix restores that exact build instead of each suite recompiling
   # the base, and ignored.yml keeps restoring the same key. `test: false` keeps
-  # this job build-only; the suites run the tests.
+  # this job build-only; the suites run the tests. It also compiles and
+  # publishes the small `nataddcomm.ixe` fixture the zkVM execution gates
+  # (sp1-build/zisk-build) run their guests over: they need this exact `ix`
+  # build, so they consume it as an artifact and gate on this job succeeding.
   build:
     name: Build Ix
     runs-on: warp-ubuntu-latest-x64-16x
@@ -72,6 +42,19 @@ jobs:
         run: lake exe ix codegen --check
       - name: Check Lean versions match for Ix and compiler bench
         run: diff lean-toolchain Benchmarks/Compile/lean-toolchain
+      # `Nat.add_comm`'s transitive-dependency closure (~40 kB, ~40 constants)
+      # is a real theorem, not an empty environment. `--consts` keeps this much
+      # smaller than the complete Init+Std environment used by benchmarks. The
+      # zkVM execution gates download this artifact and run their guests over it.
+      - name: Compile nataddcomm.ixe
+        run: lake exe ix compile Ix.lean --consts Nat.add_comm --out nataddcomm.ixe
+      - name: Upload nataddcomm.ixe
+        uses: actions/upload-artifact@v4
+        with:
+          name: nataddcomm-ixe
+          path: nataddcomm.ixe
+          if-no-files-found: error
+          retention-days: 1
 
   # Two parallel test suites over the base build the `build` job cached. Each
   # restores `.lake` rather than recompiling Ix; lean-action just provisions the
@@ -189,8 +172,8 @@ jobs:
   # failures by design (dropped rows, OOM sentinels), so they never turn red
   # on a breakage. These jobs are the red-X signal: each builds its host, then
   # runs the guest in the VM over `nataddcomm.ixe` (a ~40-constant closure the
-  # dedicated zkvm-fixture job publishes). They run in parallel with the Lean
-  # jobs and with each other after that narrow producer succeeds. Both hosts exit
+  # `build` job publishes as an artifact). They run in parallel with the test
+  # matrix and with each other after `build` succeeds. Both hosts exit
   # non-zero when the kernel rejects a constant (sp1: EXIT_REJECTED; zisk:
   # `reject_failures`), so a guest that compiles but panics / faults / rejects
   # fails the job. SP1 execute is pure RISC-V emulation (no key). Zisk execute
@@ -204,7 +187,7 @@ jobs:
   # SP1's host crates need pkg-config + libssl-dev).
   sp1-build:
     name: SP1 host build
-    needs: zkvm-fixture
+    needs: build
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7
@@ -243,7 +226,7 @@ jobs:
 
   zisk-build:
     name: Zisk host build
-    needs: zkvm-fixture
+    needs: build
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7

From dfee2391f1eeb302f712b722470c880ead0b4d23 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 16:22:05 -0400
Subject: [PATCH 3/7] ci: split test into test-core/test-tc jobs; Lean
 sorry-frontier check
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Replace the test matrix with two flat jobs — the suites shared only
checkout/toolchain setup, so the matrix body was almost entirely
`if: matrix.suite` guards. test-core (CLI + Aiur) and test-tc
(verification + parity) both `needs: build` and restore the cached base.

Replace the Perl source-token sorry audit with a Lean check
(Ix.Tc.Verify.Audit.SorryFrontier): it asks the compiler which
declarations use `sorryAx` rather than re-lexing Lean source, filters by
source module via `getModuleIdxFor?` so macro-emitted names are still
caught, and excludes upstream Lean4Lean sorries by namespace. It runs as
a `run_cmd` at elaboration (not an executable) so it never links the
blake3 and ix_ffi Rust archives, which clash on the Rust allocator.
---
 .github/scripts/check_tc_verify_sorries.pl | 212 ---------------------
 .github/workflows/ci.yml                   |  96 +++++-----
 Ix/Tc/Verify/Audit/SorryFrontier.lean      |  62 ++++++
 3 files changed, 107 insertions(+), 263 deletions(-)
 delete mode 100644 .github/scripts/check_tc_verify_sorries.pl
 create mode 100644 Ix/Tc/Verify/Audit/SorryFrontier.lean

diff --git a/.github/scripts/check_tc_verify_sorries.pl b/.github/scripts/check_tc_verify_sorries.pl
deleted file mode 100644
index 3ffcb474..00000000
--- a/.github/scripts/check_tc_verify_sorries.pl
+++ /dev/null
@@ -1,212 +0,0 @@
-#!/usr/bin/env perl
-use strict;
-use warnings;
-
-# Enforce the checked-in Ix.Tc verification sorry frontier.
-#
-# This is a source-token audit rather than a raw grep: comments and strings
-# may discuss upstream sorries without enlarging the local trusted frontier.
-# Every real Lean sorry token is attributed to its nearest top-level
-# declaration and compared with the exact allowlist below.
-
-use Cwd qw(abs_path);
-use FindBin qw($RealBin);
-use File::Find qw(find);
-use File::Spec;
-
-my $repo_root = abs_path(File::Spec->catdir($RealBin, '..', '..'));
-my $verify_root = File::Spec->catdir($repo_root, 'Ix', 'Tc', 'Verify');
-
-my %expected = ();
-
-sub mask_chunk {
-  my ($chunk) = @_;
-  $chunk =~ s/[^\n]/ /g;
-  return $chunk;
-}
-
-sub earliest {
-  my @positions = grep { $_ >= 0 } @_;
-  return -1 unless @positions;
-  my ($first) = sort { $a <=> $b } @positions;
-  return $first;
-}
-
-sub mask_non_code {
-  my ($source, $path) = @_;
-  my $length = length $source;
-  my $index = 0;
-  my $block_depth = 0;
-  my @masked;
-
-  while ($index < $length) {
-    if ($block_depth) {
-      my $open = index($source, '/-', $index);
-      my $close = index($source, '-/', $index);
-      my $next = earliest($open, $close);
-      die "$path: unterminated block comment\n" if $next < 0;
-      push @masked, mask_chunk(substr($source, $index, $next + 2 - $index));
-      if ($next == $open) {
-        ++$block_depth;
-      } else {
-        --$block_depth;
-      }
-      $index = $next + 2;
-      next;
-    }
-
-    my $line_comment = index($source, '--', $index);
-    my $block_comment = index($source, '/-', $index);
-    my $quote = index($source, '"', $index);
-    my $next = earliest($line_comment, $block_comment, $quote);
-
-    if ($next < 0) {
-      push @masked, substr($source, $index);
-      $index = $length;
-      next;
-    }
-
-    push @masked, substr($source, $index, $next - $index);
-    if ($next == $line_comment) {
-      my $newline = index($source, "\n", $next);
-      my $end = $newline < 0 ? $length : $newline;
-      push @masked, mask_chunk(substr($source, $next, $end - $next));
-      $index = $end;
-    } elsif ($next == $block_comment) {
-      push @masked, '  ';
-      $block_depth = 1;
-      $index = $next + 2;
-    } else {
-      my $closing = $next + 1;
-      while (1) {
-        $closing = index($source, '"', $closing);
-        die "$path: unterminated string literal\n" if $closing < 0;
-        my $slashes = 0;
-        my $before = $closing - 1;
-        while ($before > $next && substr($source, $before, 1) eq '\\') {
-          ++$slashes;
-          --$before;
-        }
-        last if $slashes % 2 == 0;
-        ++$closing;
-      }
-      push @masked,
-        mask_chunk(substr($source, $next, $closing + 1 - $next));
-      $index = $closing + 1;
-    }
-  }
-
-  die "$path: unterminated block comment\n" if $block_depth;
-  return join '', @masked;
-}
-
-sub relative_path {
-  my ($path) = @_;
-  my $relative = File::Spec->abs2rel($path, $repo_root);
-  $relative =~ s{\\}{/}g;
-  return $relative;
-}
-
-sub find_sorries {
-  my ($path) = @_;
-  open my $handle, '<:encoding(UTF-8)', $path
-    or die "cannot read $path: $!\n";
-  local $/;
-  my $source = <$handle>;
-  close $handle;
-
-  return () unless $source =~ /\bsorry\b/;
-  my $code = mask_non_code($source, $path);
-  my @commands;
-  while (
-    $code =~
-      m{^[ \t]*(?:(?:private|protected|noncomputable)[ \t]+)*
-        (theorem|lemma|def|opaque|abbrev|instance|inductive|structure|example)
-        [ \t]+([A-Za-z_][A-Za-z0-9_'.?]*)}mgx
-  ) {
-    push @commands, [$-[0], $1, $2];
-  }
-
-  my @found;
-  my $command_index = -1;
-  while ($code =~ /\bsorry\b/g) {
-    my $position = $-[0];
-    while (
-      $command_index + 1 < @commands
-      && $commands[$command_index + 1]->[0] < $position
-    ) {
-      ++$command_index;
-    }
-
-    my $declaration = '<no enclosing declaration>';
-    if ($command_index >= 0) {
-      my ($unused, $kind, $name) = @{$commands[$command_index]};
-      $declaration = $kind =~ /^(?:theorem|lemma)$/ ? $name : "$kind $name";
-    }
-    my $prefix = substr($source, 0, $position);
-    my $line = 1 + ($prefix =~ tr/\n//);
-    push @found, [relative_path($path), $declaration, $line];
-  }
-  return @found;
-}
-
-my @observed_with_lines;
-eval {
-  my @verify_files;
-  find(
-    {
-      no_chdir => 1,
-      wanted => sub {
-        push @verify_files, $File::Find::name
-          if -f $File::Find::name && $File::Find::name =~ /\.lean\z/;
-      },
-    },
-    $verify_root,
-  );
-  for my $path (sort @verify_files) {
-    push @observed_with_lines, find_sorries($path);
-  }
-  1;
-} or do {
-  my $error = $@ || 'unknown scan error';
-  print STDERR "tc-verify sorry audit failed to scan sources: $error";
-  exit 2;
-};
-
-my %observed;
-for my $entry (@observed_with_lines) {
-  ++$observed{"$entry->[0]\0$entry->[1]"};
-}
-
-my $matches = 1;
-for my $key (keys %expected) {
-  $matches = 0 if ($observed{$key} // 0) != $expected{$key};
-}
-for my $key (keys %observed) {
-  $matches = 0 if ($expected{$key} // 0) != $observed{$key};
-}
-
-if (!$matches) {
-  print STDERR "Ix.Tc Verify sorry frontier changed.\n";
-  print STDERR "Expected:\n";
-  for my $key (sort keys %expected) {
-    my ($path, $declaration) = split /\0/, $key, 2;
-    print STDERR "  $expected{$key} x $path :: $declaration\n";
-  }
-  print STDERR "Observed:\n";
-  if (@observed_with_lines) {
-    for my $entry (@observed_with_lines) {
-      print STDERR "  $entry->[0]:$entry->[2] :: $entry->[1]\n";
-    }
-  } else {
-    print STDERR "  <none>\n";
-  }
-  print STDERR
-    "Update the allowlist only when the formal trust frontier intentionally changes.\n";
-  exit 1;
-}
-
-print "Ix.Tc Verify sorry frontier OK:\n";
-for my $entry (@observed_with_lines) {
-  print "  $entry->[0]:$entry->[2] :: $entry->[1]\n";
-}
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a0bca81f..98419043 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -16,9 +16,10 @@ concurrency:
 jobs:
   # Build Ix once — with the --wfail lint gate over every lib/exe target — and
   # let lean-action cache the full `.lake` under its per-sha key. The parallel
-  # `test` matrix restores that exact build instead of each suite recompiling
-  # the base, and ignored.yml keeps restoring the same key. `test: false` keeps
-  # this job build-only; the suites run the tests. It also compiles and
+  # test-core / test-tc jobs restore that exact build instead of each one
+  # recompiling the base, and ignored.yml keeps restoring the same key.
+  # `test: false` keeps this job build-only; those jobs run the tests. It also
+  # compiles and
   # publishes the small `nataddcomm.ixe` fixture the zkVM execution gates
   # (sp1-build/zisk-build) run their guests over: they need this exact `ix`
   # build, so they consume it as an artifact and gate on this job succeeding.
@@ -35,7 +36,7 @@ jobs:
       # build-all lint driver compiles every lib/exe target with --wfail, so a
       # warning in any target (exes, benchmarks, Apps) — not just the default lib
       # lean-action builds above — fails CI. Building them here also populates
-      # the cache the test matrix restores.
+      # the cache the test-core / test-tc jobs restore.
       - name: Build all targets
         run: lake lint -- --wfail -v
       - name: Check codegen'd IxVM kernel is up to date
@@ -56,42 +57,47 @@ jobs:
           if-no-files-found: error
           retention-days: 1
 
-  # Two parallel test suites over the base build the `build` job cached. Each
-  # restores `.lake` rather than recompiling Ix; lean-action just provisions the
-  # toolchain (no build/cache) and the suite's `lake test` steps run against the
-  # restored build. The tc suite's heavyweight secondary work — the ~13-min
-  # `Ix.Tc.Verify` proof elaboration and parity run — is what keeps the split
-  # worthwhile: it overlaps the core suite instead of serializing behind it.
-  test:
+  # CLI + Aiur tests over the base build the `build` job cached. Restores
+  # `.lake` read-only (exact per-sha key the `build` job wrote, prefix fallback
+  # otherwise); lean-action just provisions the toolchain (no build/cache) and
+  # the `lake test` steps run against the restored build.
+  test-core:
+    name: CLI and Aiur tests
     needs: build
-    name: ${{ matrix.name }}
     runs-on: warp-ubuntu-latest-x64-16x
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - suite: core
-            name: CLI and Aiur tests
-          - suite: tc
-            name: Ix.Tc verification and parity
     steps:
       - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
-      # Core restores the base build read-only (exact per-sha key the `build`
-      # job wrote, prefix fallback otherwise).
-      - if: matrix.suite == 'core'
-        uses: actions/cache/restore@v6
+      - uses: actions/cache/restore@v6
         with:
           path: .lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
-      # The tc suite keeps its own `lake-tc-…` cache so it can additionally
-      # persist the proof elaboration across commits: restore its latest prior
-      # build first, fall back to the base build, and save the proof-laden
-      # `.lake` at job end. Correctness is Lake's — a stale restore forces a
-      # rebuild via per-module traces, never a wrong olean.
-      - if: matrix.suite == 'tc'
-        uses: actions/cache@v6
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - name: Test Ix CLI
+        run: lake test --wfail -- cli
+      - name: Aiur tests
+        run: lake test --wfail -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier
+
+  # Ix.Tc verification + parity over the base build. Its heavyweight work — the
+  # ~13-min `Ix.Tc.Verify` proof elaboration and the parity run — is what keeps
+  # this split from test-core worthwhile: it overlaps that suite instead of
+  # serializing behind it. Unlike test-core this keeps its own `lake-tc-…` cache
+  # so it can additionally persist the proof elaboration across commits: restore
+  # its latest prior build first, fall back to the base build, and save the
+  # proof-laden `.lake` at job end. Correctness is Lake's — a stale restore
+  # forces a rebuild via per-module traces, never a wrong olean.
+  test-tc:
+    name: Ix.Tc verification and parity
+    needs: build
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v7
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      - uses: actions/cache@v6
         with:
           path: .lake
           key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
@@ -102,26 +108,15 @@ jobs:
         with:
           auto-config: false
           use-github-cache: false
-      - if: matrix.suite == 'core'
-        name: Test Ix CLI
-        run: lake test --wfail -- cli
-      - if: matrix.suite == 'core'
-        name: Aiur tests
-        run: lake test --wfail -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier
-      - if: matrix.suite == 'tc'
-        name: Check Ix.Tc verification sorry frontier
-        run: perl .github/scripts/check_tc_verify_sorries.pl
-      - if: matrix.suite == 'tc'
-        name: Check Ix.Tc exported theorem trust manifest
+      - name: Check Ix.Tc exported theorem trust manifest
         run: lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Statements
-      - if: matrix.suite == 'tc'
-        name: Build Ix.Tc formal verification
+      - name: Build Ix.Tc formal verification
         run: lake build IxTcVerify
-      - if: matrix.suite == 'tc'
-        name: Test Ix.Tc unit and adversarial fixtures
+      - name: Check Ix.Tc verification sorry frontier
+        run: lake build Ix.Tc.Verify.Audit.SorryFrontier
+      - name: Test Ix.Tc unit and adversarial fixtures
         run: lake test --wfail -- tc-unit
-      - if: matrix.suite == 'tc'
-        name: Compile Ix.Tc parity fixture
+      - name: Compile Ix.Tc parity fixture
         run: >-
           lake exe ix compile Ix.lean
           --consts-file .github/fixtures/tc-parity-consts.txt
@@ -129,8 +124,7 @@ jobs:
       # The verification release claim includes executable adversarial and
       # production-parity evidence. Its exact pin/accelerator seed closure is
       # deliberately separate from the much smaller zkVM smoke fixture.
-      - if: matrix.suite == 'tc'
-        name: Test Ix.Tc production parity and scale
+      - name: Test Ix.Tc production parity and scale
         run: >-
           lake test --wfail -- --ignored
           tc-pins tc-accel-diff tc-anon-diff tc-roundtrip tc-init
@@ -173,7 +167,7 @@ jobs:
   # on a breakage. These jobs are the red-X signal: each builds its host, then
   # runs the guest in the VM over `nataddcomm.ixe` (a ~40-constant closure the
   # `build` job publishes as an artifact). They run in parallel with the test
-  # matrix and with each other after `build` succeeds. Both hosts exit
+  # jobs and with each other after `build` succeeds. Both hosts exit
   # non-zero when the kernel rejects a constant (sp1: EXIT_REJECTED; zisk:
   # `reject_failures`), so a guest that compiles but panics / faults / rejects
   # fails the job. SP1 execute is pure RISC-V emulation (no key). Zisk execute
diff --git a/Ix/Tc/Verify/Audit/SorryFrontier.lean b/Ix/Tc/Verify/Audit/SorryFrontier.lean
new file mode 100644
index 00000000..28aa23ef
--- /dev/null
+++ b/Ix/Tc/Verify/Audit/SorryFrontier.lean
@@ -0,0 +1,62 @@
+import Ix.Tc.Verify.Audit.Completed
+import Ix.Tc.Verify.Audit.Statements
+
+/-!
+# `Ix.Tc.Verify` source sorry frontier
+
+Fail the build if any declaration defined in an `Ix.Tc.Verify` source module
+directly uses `sorryAx` — the elaborated form of a `sorry` token in that
+source. The compiler answers this from the checked environment, so unlike a
+source-token grep it can never drift from Lean's syntax (comments, string/char
+literals, nested block comments). Filtering is by SOURCE MODULE via
+`getModuleIdxFor?`, not declaration name, so macro-emitted constants registered
+under unqualified names are still attributed to their host module. Upstream
+(Lean4Lean) `sorryAx` users are excluded because they live outside the
+`Ix.Tc.Verify` namespace — the distinction `lake build --wfail` cannot make.
+
+Runs as a `run_cmd` at elaboration, next to the trust manifest it complements
+(`Ix.Tc.Verify.Audit.check`): a build-time command, not an executable, so it
+never links the Rust FFI archives an exe over these modules would clash on.
+Importing the audit roots pulls the verified surface into scope; a declaration
+in a Verify module not reachable from those roots is not checked here.
+-/
+
+open Lean Lean.Elab.Command
+
+namespace Ix.Tc.Verify.Audit
+
+/-- Constants referenced directly by a declaration's type or value, following
+the same cases as `Lean.collectAxioms`. The `Lean.` qualifiers are load-bearing:
+the imported Ix kernel defines its own `Name`/`ConstantInfo` that shadow Lean's
+inside this namespace. -/
+private def sorryFrontierDirectConstants : Lean.ConstantInfo → Array Lean.Name
+  | .axiomInfo v => v.type.getUsedConstants
+  | .defnInfo v => v.type.getUsedConstants ++ v.value.getUsedConstants
+  | .thmInfo v => v.type.getUsedConstants ++ v.value.getUsedConstants
+  | .opaqueInfo v => v.type.getUsedConstants ++ v.value.getUsedConstants
+  | .quotInfo _ => #[]
+  | .ctorInfo v => v.type.getUsedConstants
+  | .recInfo v => v.type.getUsedConstants
+  | .inductInfo v => v.type.getUsedConstants ++ v.ctors
+
+/-- Fail if any `Ix.Tc.Verify` source declaration directly references `sorryAx`. -/
+def checkSorryFrontier : CommandElabM Unit := do
+  let env ← getEnv
+  let moduleNames := env.allImportedModuleNames
+  let offenders := env.constants.toList.filterMap fun (name, info) =>
+    match env.getModuleIdxFor? name with
+    | none => none
+    | some idx =>
+      let mod := moduleNames[idx.toNat]!
+      if (`Ix.Tc.Verify).isPrefixOf mod && (sorryFrontierDirectConstants info).contains ``sorryAx then some (mod, name) else none
+  let offenders := offenders.toArray.qsort (fun a b => Lean.Name.lt a.1 b.1)
+  if offenders.isEmpty then
+    logInfo m!"Ix.Tc.Verify sorry frontier OK: no source declaration uses sorryAx"
+  else
+    let body := String.intercalate "\n"
+      (offenders.toList.map fun (mod, name) => s!"  {mod} :: {name}")
+    throwError m!"Ix.Tc.Verify sorry frontier changed — {offenders.size} declaration(s) directly use sorryAx:\n{body}\nResolve the sorry, or extend the Ix.Tc.Verify.Audit trust manifest, only when the verification frontier intentionally changes."
+
+run_cmd checkSorryFrontier
+
+end Ix.Tc.Verify.Audit

From bdc9f3ca1c5f906c4e4c67f1dddf88cdfb084846 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 17:54:29 -0400
Subject: [PATCH 4/7] ci: run the Ix.Tc verification suite on push-to-main only
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Move the typechecker job out of ci.yml (which runs per-PR) into
ignored.yml's Extended CI tests (push-to-main + workflow_dispatch),
renamed test-tc -> tc-test. The ~13-min Ix.Tc.Verify proof elaboration
and parity run no longer gate every PR; they run once per merge on main.

The job keeps its own lake-tc cache (restore + save, falling back to
ci.yml's base build) so the proof elaboration stays incremental across
main commits — worthwhile at 1-4 merges/day.

Note: the "Ix.Tc verification and parity" check no longer runs on PRs, so
remove it from any required-PR-checks branch protection.
---
 .github/workflows/ci.yml      | 56 ++---------------------------------
 .github/workflows/ignored.yml | 48 ++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+), 53 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 98419043..1238d69a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -16,8 +16,8 @@ concurrency:
 jobs:
   # Build Ix once — with the --wfail lint gate over every lib/exe target — and
   # let lean-action cache the full `.lake` under its per-sha key. The parallel
-  # test-core / test-tc jobs restore that exact build instead of each one
-  # recompiling the base, and ignored.yml keeps restoring the same key.
+  # test-core job restores that exact build instead of recompiling the base, as
+  # do ignored.yml's extended jobs (including the push-to-main-only Ix.Tc suite).
   # `test: false` keeps this job build-only; those jobs run the tests. It also
   # compiles and
   # publishes the small `nataddcomm.ixe` fixture the zkVM execution gates
@@ -36,7 +36,7 @@ jobs:
       # build-all lint driver compiles every lib/exe target with --wfail, so a
       # warning in any target (exes, benchmarks, Apps) — not just the default lib
       # lean-action builds above — fails CI. Building them here also populates
-      # the cache the test-core / test-tc jobs restore.
+      # the cache the test-core job and ignored.yml's extended jobs restore.
       - name: Build all targets
         run: lake lint -- --wfail -v
       - name: Check codegen'd IxVM kernel is up to date
@@ -82,56 +82,6 @@ jobs:
       - name: Aiur tests
         run: lake test --wfail -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier
 
-  # Ix.Tc verification + parity over the base build. Its heavyweight work — the
-  # ~13-min `Ix.Tc.Verify` proof elaboration and the parity run — is what keeps
-  # this split from test-core worthwhile: it overlaps that suite instead of
-  # serializing behind it. Unlike test-core this keeps its own `lake-tc-…` cache
-  # so it can additionally persist the proof elaboration across commits: restore
-  # its latest prior build first, fall back to the base build, and save the
-  # proof-laden `.lake` at job end. Correctness is Lake's — a stale restore
-  # forces a rebuild via per-module traces, never a wrong olean.
-  test-tc:
-    name: Ix.Tc verification and parity
-    needs: build
-    runs-on: warp-ubuntu-latest-x64-16x
-    steps:
-      - uses: actions/checkout@v7
-      - uses: actions-rust-lang/setup-rust-toolchain@v1
-      - uses: actions/cache@v6
-        with:
-          path: .lake
-          key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: |
-            lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
-            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
-      - uses: leanprover/lean-action@v1
-        with:
-          auto-config: false
-          use-github-cache: false
-      - name: Check Ix.Tc exported theorem trust manifest
-        run: lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Statements
-      - name: Build Ix.Tc formal verification
-        run: lake build IxTcVerify
-      - name: Check Ix.Tc verification sorry frontier
-        run: lake build Ix.Tc.Verify.Audit.SorryFrontier
-      - name: Test Ix.Tc unit and adversarial fixtures
-        run: lake test --wfail -- tc-unit
-      - name: Compile Ix.Tc parity fixture
-        run: >-
-          lake exe ix compile Ix.lean
-          --consts-file .github/fixtures/tc-parity-consts.txt
-          --out tc-parity.ixe
-      # The verification release claim includes executable adversarial and
-      # production-parity evidence. Its exact pin/accelerator seed closure is
-      # deliberately separate from the much smaller zkVM smoke fixture.
-      - name: Test Ix.Tc production parity and scale
-        run: >-
-          lake test --wfail -- --ignored
-          tc-pins tc-accel-diff tc-anon-diff tc-roundtrip tc-init
-          tc-tutorial lean4lean
-        env:
-          IX_PINS_IXE: tc-parity.ixe
-
   rust-test:
     runs-on: ubuntu-latest
     steps:
diff --git a/.github/workflows/ignored.yml b/.github/workflows/ignored.yml
index 37f49f45..e81043d9 100644
--- a/.github/workflows/ignored.yml
+++ b/.github/workflows/ignored.yml
@@ -69,3 +69,51 @@ jobs:
             --error-exitcode=1 \
             --suppressions=.github/valgrind.supp \
             .lake/build/bin/IxTests -- ffi
+
+  # Ix.Tc formal verification + typechecker parity suite. Lives here (push to
+  # main / dispatch only) rather than in ci.yml so its ~13-min `Ix.Tc.Verify`
+  # proof elaboration and parity run don't gate every PR. Restores the base
+  # `.lake` that ci.yml's build job saved (via the `lake-…` fallback) and keeps
+  # its own `lake-tc-…` cache so the proof elaboration persists across main
+  # commits; lean-action provides only the toolchain, and the steps build/test
+  # against the restored `.lake`.
+  tc-test:
+    name: Ix.Tc verification and parity
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v7
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      - uses: actions/cache@v6
+        with:
+          path: .lake
+          key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: |
+            lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - name: Check Ix.Tc exported theorem trust manifest
+        run: lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Statements
+      - name: Build Ix.Tc formal verification
+        run: lake build IxTcVerify
+      - name: Check Ix.Tc verification sorry frontier
+        run: lake build Ix.Tc.Verify.Audit.SorryFrontier
+      - name: Test Ix.Tc unit and adversarial fixtures
+        run: lake test --wfail -- tc-unit
+      - name: Compile Ix.Tc parity fixture
+        run: >-
+          lake exe ix compile Ix.lean
+          --consts-file .github/fixtures/tc-parity-consts.txt
+          --out tc-parity.ixe
+      # The verification release claim includes executable adversarial and
+      # production-parity evidence. Its exact pin/accelerator seed closure is
+      # deliberately separate from the much smaller zkVM smoke fixture.
+      - name: Test Ix.Tc production parity and scale
+        run: >-
+          lake test --wfail -- --ignored
+          tc-pins tc-accel-diff tc-anon-diff tc-roundtrip tc-init
+          tc-tutorial lean4lean
+        env:
+          IX_PINS_IXE: tc-parity.ixe

From f2bb5512f9a3d13e1e3277610dcebf9512c49b34 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 18:06:11 -0400
Subject: [PATCH 5/7] ci: retry the zkVM apt install to survive transient
 mirror errors
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The shared zkVM system-deps install (install-zisk/install-sp1) sporadically
fails on transient Ubuntu EC2 mirror errors — e.g. a 502 Bad Gateway fetching
qemu-system — reding the whole zkVM job. Wrap update+install in a 3-attempt
retry loop with backoff, add `-o Acquire::Retries=5` for single-download
blips and `--fix-missing` to resume a partial fetch, and fail explicitly
after the last attempt.
---
 .github/actions/install-sp1/action.yml  | 28 ++++++++++++++++++-------
 .github/actions/install-zisk/action.yml | 28 ++++++++++++++++++-------
 .github/workflows/ci.yml                |  2 +-
 3 files changed, 43 insertions(+), 15 deletions(-)

diff --git a/.github/actions/install-sp1/action.yml b/.github/actions/install-sp1/action.yml
index de09bf64..2b151d47 100644
--- a/.github/actions/install-sp1/action.yml
+++ b/.github/actions/install-sp1/action.yml
@@ -16,13 +16,27 @@ runs:
         # Some warpbuild images ship an unreachable azure mirror that hangs
         # `apt-get update`; drop it first (no-op elsewhere).
         sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true
-        sudo apt-get update
-        sudo apt-get install -y \
-          xz-utils jq curl build-essential qemu-system libomp-dev libgmp-dev \
-          nlohmann-json3-dev protobuf-compiler uuid-dev libgrpc++-dev \
-          libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
-          openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
-          pkg-config libssl-dev
+        export DEBIAN_FRONTEND=noninteractive
+        # The Ubuntu EC2 mirrors sporadically 502 / throttle on these large
+        # fetches (qemu-system alone pulls hundreds of MB), so retry the whole
+        # update+install: `Acquire::Retries` absorbs single-download blips and
+        # `--fix-missing` resumes a partially fetched set.
+        for attempt in 1 2 3; do
+          sudo apt-get update || true
+          if sudo apt-get install -y --fix-missing -o Acquire::Retries=5 \
+            xz-utils jq curl build-essential qemu-system libomp-dev libgmp-dev \
+            nlohmann-json3-dev protobuf-compiler uuid-dev libgrpc++-dev \
+            libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
+            openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
+            pkg-config libssl-dev; then
+            break
+          fi
+          if [ "$attempt" = 3 ]; then
+            echo "::error::apt-get install failed after 3 attempts"; exit 1
+          fi
+          echo "::warning::apt-get install attempt $attempt failed; retrying in $((attempt * 20))s"
+          sleep $((attempt * 20))
+        done
     # sp1up resolves `releases/latest` (and downloads the toolchain) through
     # api.github.com. Anonymous API calls share a 60/hr per-IP limit that hot
     # runner IPs exhaust, failing the step with "Unable to access the latest
diff --git a/.github/actions/install-zisk/action.yml b/.github/actions/install-zisk/action.yml
index 84b98dd0..1b1c0250 100644
--- a/.github/actions/install-zisk/action.yml
+++ b/.github/actions/install-zisk/action.yml
@@ -29,13 +29,27 @@ runs:
         # Some warpbuild images ship an unreachable azure mirror that hangs
         # `apt-get update`; drop it first (no-op elsewhere).
         sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true
-        sudo apt-get update
-        sudo apt-get install -y \
-          xz-utils jq curl build-essential qemu-system libomp-dev libgmp-dev \
-          nlohmann-json3-dev protobuf-compiler uuid-dev libgrpc++-dev \
-          libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
-          openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
-          pkg-config libssl-dev
+        export DEBIAN_FRONTEND=noninteractive
+        # The Ubuntu EC2 mirrors sporadically 502 / throttle on these large
+        # fetches (qemu-system alone pulls hundreds of MB), so retry the whole
+        # update+install: `Acquire::Retries` absorbs single-download blips and
+        # `--fix-missing` resumes a partially fetched set.
+        for attempt in 1 2 3; do
+          sudo apt-get update || true
+          if sudo apt-get install -y --fix-missing -o Acquire::Retries=5 \
+            xz-utils jq curl build-essential qemu-system libomp-dev libgmp-dev \
+            nlohmann-json3-dev protobuf-compiler uuid-dev libgrpc++-dev \
+            libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
+            openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
+            pkg-config libssl-dev; then
+            break
+          fi
+          if [ "$attempt" = 3 ]; then
+            echo "::error::apt-get install failed after 3 attempts"; exit 1
+          fi
+          echo "::warning::apt-get install attempt $attempt failed; retrying in $((attempt * 20))s"
+          sleep $((attempt * 20))
+        done
     # Host links the argumentcomputer/zisk fork (check-setup lives in the
     # `cargo-zisk-dev` binary, used below to regenerate the key's
     # const-trees). `--cpu` picks
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 1238d69a..c935881a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -24,7 +24,7 @@ jobs:
   # (sp1-build/zisk-build) run their guests over: they need this exact `ix`
   # build, so they consume it as an artifact and gate on this job succeeding.
   build:
-    name: Build Ix
+    name: lean-test
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7

From 77e50750389e7f6b7737ad9c8c26d308e64cb1ab Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 19:31:00 -0400
Subject: [PATCH 6/7] ci: use ./.lake cache path to match lean-action
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The .lake cache consumers (lean-test in ci.yml; ignored-test, valgrind-ffi,
and tc-test in ignored.yml) restored with `path: .lake`, but lean-action saves
under `path: ./.lake`. GitHub hashes the path into a cache entry's version, so
the restore computed a different version and missed despite a byte-identical
key — the entry existed but was never read, forcing a full rebuild. Align the
consumers to ./.lake.
---
 .github/workflows/ci.yml      | 6 +++++-
 .github/workflows/ignored.yml | 6 +++---
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c935881a..a0e83209 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -68,9 +68,13 @@ jobs:
     steps:
       - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
+      # `./.lake`, not `.lake`: the cache path is hashed into the entry's
+      # version, and lean-action saves under `./.lake`, so a bare `.lake` here
+      # computes a different version and the restore misses despite the key
+      # matching.
       - uses: actions/cache/restore@v6
         with:
-          path: .lake
+          path: ./.lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
       - uses: leanprover/lean-action@v1
diff --git a/.github/workflows/ignored.yml b/.github/workflows/ignored.yml
index e81043d9..ca15bca9 100644
--- a/.github/workflows/ignored.yml
+++ b/.github/workflows/ignored.yml
@@ -21,7 +21,7 @@ jobs:
       # Only restore the cache, since `ci.yml` will save the test binary to the cache first
       - uses: actions/cache/restore@v6
         with:
-          path: .lake
+          path: ./.lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
       - uses: leanprover/lean-action@v1
@@ -43,7 +43,7 @@ jobs:
       # Only restore the cache, since `ci.yml` will save the test binary to the cache first
       - uses: actions/cache/restore@v6
         with:
-          path: .lake
+          path: ./.lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
       - uses: leanprover/lean-action@v1
@@ -85,7 +85,7 @@ jobs:
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       - uses: actions/cache@v6
         with:
-          path: .lake
+          path: ./.lake
           key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: |
             lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-

From 0f3d6428b50d34a8a7254e1a0eba3a89b6816b4d Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 19:32:01 -0400
Subject: [PATCH 7/7] test(tc): compile the parity env on demand; rename test
 job; CI tidy

- tc-pins / tc-accel-diff compile their `.ixe` env on demand
  (Tests.Tc.ParityEnv) rather than silently skipping when IX_PINS_IXE is
  unset; add a `--exclude` test-runner flag so ignored-test and tc-test
  partition the ignored suites with no duplication.
- report the CI build job's check as `lean-test` (matches branch protection).
- correct the build/lint cache comments and the nix flake-check catch-all
  comment; tidy the SorryFrontier docstring.
- shorten the zkVM apt-install retry backoff to 10s.
---
 .github/actions/install-sp1/action.yml  |  4 +-
 .github/actions/install-zisk/action.yml |  4 +-
 .github/workflows/ci.yml                | 25 +++----
 .github/workflows/ignored.yml           | 35 ++++------
 .github/workflows/nix.yml               |  5 +-
 Ix/Tc/Verify/Audit/SorryFrontier.lean   |  6 +-
 Tests/Ix/Tc/AccelDiff.lean              | 11 ++-
 Tests/Ix/Tc/ParityEnv.lean              | 90 +++++++++++++++++++++++++
 Tests/Ix/Tc/Pins.lean                   | 16 ++---
 Tests/Main.lean                         | 39 ++++++-----
 10 files changed, 159 insertions(+), 76 deletions(-)
 create mode 100644 Tests/Ix/Tc/ParityEnv.lean

diff --git a/.github/actions/install-sp1/action.yml b/.github/actions/install-sp1/action.yml
index 2b151d47..5f820cd0 100644
--- a/.github/actions/install-sp1/action.yml
+++ b/.github/actions/install-sp1/action.yml
@@ -34,8 +34,8 @@ runs:
           if [ "$attempt" = 3 ]; then
             echo "::error::apt-get install failed after 3 attempts"; exit 1
           fi
-          echo "::warning::apt-get install attempt $attempt failed; retrying in $((attempt * 20))s"
-          sleep $((attempt * 20))
+          echo "::warning::apt-get install attempt $attempt failed; retrying in $((attempt * 10))s"
+          sleep $((attempt * 10))
         done
     # sp1up resolves `releases/latest` (and downloads the toolchain) through
     # api.github.com. Anonymous API calls share a 60/hr per-IP limit that hot
diff --git a/.github/actions/install-zisk/action.yml b/.github/actions/install-zisk/action.yml
index 1b1c0250..1dfcc4ca 100644
--- a/.github/actions/install-zisk/action.yml
+++ b/.github/actions/install-zisk/action.yml
@@ -47,8 +47,8 @@ runs:
           if [ "$attempt" = 3 ]; then
             echo "::error::apt-get install failed after 3 attempts"; exit 1
           fi
-          echo "::warning::apt-get install attempt $attempt failed; retrying in $((attempt * 20))s"
-          sleep $((attempt * 20))
+          echo "::warning::apt-get install attempt $attempt failed; retrying in $((attempt * 10))s"
+          sleep $((attempt * 10))
         done
     # Host links the argumentcomputer/zisk fork (check-setup lives in the
     # `cargo-zisk-dev` binary, used below to regenerate the key's
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a0e83209..952e4d27 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -14,17 +14,16 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  # Build Ix once — with the --wfail lint gate over every lib/exe target — and
-  # let lean-action cache the full `.lake` under its per-sha key. The parallel
-  # test-core job restores that exact build instead of recompiling the base, as
-  # do ignored.yml's extended jobs (including the push-to-main-only Ix.Tc suite).
-  # `test: false` keeps this job build-only; those jobs run the tests. It also
-  # compiles and
-  # publishes the small `nataddcomm.ixe` fixture the zkVM execution gates
-  # (sp1-build/zisk-build) run their guests over: they need this exact `ix`
-  # build, so they consume it as an artifact and gate on this job succeeding.
+  # Build Ix once and cache `.lake` under lean-action's per-sha key. That cache
+  # holds the base Ix build — lean-action saves it right after building the
+  # default lib, before the all-targets lint below — and the parallel lean-test
+  # job and ignored.yml's extended jobs restore it instead of recompiling the
+  # base. `test: false` keeps this job build-only; those jobs run the tests. It
+  # also compiles and publishes the small `nataddcomm.ixe` fixture the zkVM
+  # execution gates (sp1-build/zisk-build) run their guests over: they need this
+  # exact `ix` build, so they consume it as an artifact and gate on this job
+  # succeeding.
   build:
-    name: lean-test
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7
@@ -35,8 +34,7 @@ jobs:
           test: false
       # build-all lint driver compiles every lib/exe target with --wfail, so a
       # warning in any target (exes, benchmarks, Apps) — not just the default lib
-      # lean-action builds above — fails CI. Building them here also populates
-      # the cache the test-core job and ignored.yml's extended jobs restore.
+      # lean-action builds above — fails CI.
       - name: Build all targets
         run: lake lint -- --wfail -v
       - name: Check codegen'd IxVM kernel is up to date
@@ -61,8 +59,7 @@ jobs:
   # `.lake` read-only (exact per-sha key the `build` job wrote, prefix fallback
   # otherwise); lean-action just provisions the toolchain (no build/cache) and
   # the `lake test` steps run against the restored build.
-  test-core:
-    name: CLI and Aiur tests
+  lean-test:
     needs: build
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
diff --git a/.github/workflows/ignored.yml b/.github/workflows/ignored.yml
index ca15bca9..1d4f1c41 100644
--- a/.github/workflows/ignored.yml
+++ b/.github/workflows/ignored.yml
@@ -32,7 +32,9 @@ jobs:
           # test: true
           # test-args: "-- --ignored"
           use-github-cache: false
-      - run: lake test -- --ignored
+      - run: >-
+          lake test -- --ignored
+          --exclude=tc-pins,tc-accel-diff,tc-anon-diff,tc-init,tc-tutorial,tc-roundtrip,lean4lean
       - run: lake exe Apps.ZKVoting.Prover
 
   valgrind-ffi:
@@ -70,13 +72,12 @@ jobs:
             --suppressions=.github/valgrind.supp \
             .lake/build/bin/IxTests -- ffi
 
-  # Ix.Tc formal verification + typechecker parity suite. Lives here (push to
-  # main / dispatch only) rather than in ci.yml so its ~13-min `Ix.Tc.Verify`
-  # proof elaboration and parity run don't gate every PR. Restores the base
-  # `.lake` that ci.yml's build job saved (via the `lake-…` fallback) and keeps
-  # its own `lake-tc-…` cache so the proof elaboration persists across main
-  # commits; lean-action provides only the toolchain, and the steps build/test
-  # against the restored `.lake`.
+  # Ix.Tc formal verification + typechecker parity suite, run on push-to-main
+  # and manual dispatch only so its ~13-min `Ix.Tc.Verify` proof elaboration and
+  # parity run don't gate PRs. Restores the base `.lake` that ci.yml's build job
+  # saved (via the `lake-…` fallback) and keeps its own `lake-tc-…` cache so the
+  # proof elaboration persists across main commits; lean-action provides only the
+  # toolchain, and the steps build/test against the restored `.lake`.
   tc-test:
     name: Ix.Tc verification and parity
     runs-on: warp-ubuntu-latest-x64-16x
@@ -102,18 +103,10 @@ jobs:
         run: lake build Ix.Tc.Verify.Audit.SorryFrontier
       - name: Test Ix.Tc unit and adversarial fixtures
         run: lake test --wfail -- tc-unit
-      - name: Compile Ix.Tc parity fixture
-        run: >-
-          lake exe ix compile Ix.lean
-          --consts-file .github/fixtures/tc-parity-consts.txt
-          --out tc-parity.ixe
-      # The verification release claim includes executable adversarial and
-      # production-parity evidence. Its exact pin/accelerator seed closure is
-      # deliberately separate from the much smaller zkVM smoke fixture.
-      - name: Test Ix.Tc production parity and scale
+      # These ignored typechecker suites run only here; the ignored-test job
+      # --excludes them so nothing is duplicated. tc-pins / tc-accel-diff
+      # compile their `.ixe` env on demand (see Tests.Tc.ParityEnv).
+      - name: Test Ix.Tc ignored suites
         run: >-
           lake test --wfail -- --ignored
-          tc-pins tc-accel-diff tc-anon-diff tc-roundtrip tc-init
-          tc-tutorial lean4lean
-        env:
-          IX_PINS_IXE: tc-parity.ixe
+          tc-pins tc-accel-diff tc-anon-diff tc-init tc-tutorial tc-roundtrip lean4lean
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index 1221b49f..80f280f9 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -36,8 +36,9 @@ jobs:
       - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.clippy
       - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.nextest
       - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.ix-tests
-      # Catch-all: near-free after the steps above; fails if a check is added
-      # to the flake without a step here.
+      # Catch-all: builds every flake check for this system (near-free — the
+      # heavy ones above are already in the store), so a check added without
+      # its own step is still verified here.
       - run: nix flake check --accept-flake-config
 
   # Tests Nix devShell support on Ubuntu
diff --git a/Ix/Tc/Verify/Audit/SorryFrontier.lean b/Ix/Tc/Verify/Audit/SorryFrontier.lean
index 28aa23ef..cad98b7e 100644
--- a/Ix/Tc/Verify/Audit/SorryFrontier.lean
+++ b/Ix/Tc/Verify/Audit/SorryFrontier.lean
@@ -6,9 +6,9 @@ import Ix.Tc.Verify.Audit.Statements
 
 Fail the build if any declaration defined in an `Ix.Tc.Verify` source module
 directly uses `sorryAx` — the elaborated form of a `sorry` token in that
-source. The compiler answers this from the checked environment, so unlike a
-source-token grep it can never drift from Lean's syntax (comments, string/char
-literals, nested block comments). Filtering is by SOURCE MODULE via
+source. Reading it from the checked environment means `sorry` tokens in
+comments, string/char literals, or nested block comments cannot cause false
+positives. Filtering is by SOURCE MODULE via
 `getModuleIdxFor?`, not declaration name, so macro-emitted constants registered
 under unqualified names are still attributed to their host module. Upstream
 (Lean4Lean) `sorryAx` users are excluded because they live outside the
diff --git a/Tests/Ix/Tc/AccelDiff.lean b/Tests/Ix/Tc/AccelDiff.lean
index a1fdf9c1..e9f096ae 100644
--- a/Tests/Ix/Tc/AccelDiff.lean
+++ b/Tests/Ix/Tc/AccelDiff.lean
@@ -2,6 +2,7 @@ module
 
 public import LSpec
 public import Ix.Tc
+public import Tests.Ix.Tc.ParityEnv
 
 /-!
 `tc-accel-diff` (ignored runner): differential fixtures for the
@@ -10,8 +11,9 @@ CLI `IX_TC_NO_ACCEL=1`). The accelerations are shared trusted code in
 BOTH kernels (BitVec natives, Decidable natives, `reduceBool`/`reduceNat`
 markers, `Fin.val`-through-`Decidable.rec`), so cross-kernel diffing is
 structurally blind to a common bug — these fixtures check accelerated
-results against genuine pure reduction over the real env
-(`IX_PINS_IXE`; the pure path needs real definitions to delta-unfold).
+results against genuine pure reduction over the real env (compiled on
+demand — see `Tests.Tc.ParityEnv`; the pure path needs real definitions
+to delta-unfold).
 Small literals only: the pure path is exponential in literal size by
 design (see `TcState.noAccel`).
 
@@ -71,10 +73,7 @@ def ctorCase (ixonEnv : Ixon.Env) (name : String) (e : AE)
 
 public def run : IO UInt32 := do
   IO.println "tc-accel-diff"
-  let some path ← IO.getEnv "IX_PINS_IXE"
-    | IO.println "tc-accel-diff: IX_PINS_IXE unset — skipping (needs a \
-                  compileinitstd-style .ixe for the pure path's definitions)"
-      return 0
+  let path ← Tests.Tc.ParityEnv.ensure
   let bytes ← IO.FS.readBinFile path
   match Ixon.deEnvAnon bytes with
   | .error e =>
diff --git a/Tests/Ix/Tc/ParityEnv.lean b/Tests/Ix/Tc/ParityEnv.lean
new file mode 100644
index 00000000..fcd961c4
--- /dev/null
+++ b/Tests/Ix/Tc/ParityEnv.lean
@@ -0,0 +1,90 @@
+module
+
+-- Private imports: `ensure`'s signature is just `IO FilePath`; these provide
+-- only its implementation. `Ix.Meta` re-exports `getFileEnv` and `Ix.CompileM`
+-- (`rsCompileEnvBytesFFI`). The transitive dep closure is inlined below rather
+-- than taken from `Ix.Cli.ValidateCmd`, whose top-level `collectDeps` collides
+-- with the same-named def in `Tests.Ix.Compile.ValidateAux` once both reach
+-- Main.
+import Ix.Meta
+import Ix.Cli.ConstsFile
+
+/-!
+Shared fixture for the typechecker parity tests (`tc-pins`, `tc-accel-diff`):
+the serialized `.ixe` env they check against. Compiled on demand from `Ix.lean`
+plus the checked-in seed list when the file isn't already present, so the tests
+run unconditionally instead of skipping when no fixture is supplied.
+-/
+
+namespace Tests.Tc.ParityEnv
+
+open Lean
+
+/-- Transitive dependency closure of `seeds` in `env` — the constants a compiled
+`.ixe` must contain. Mirrors `Ix.Cli.ValidateCmd.collectDeps`. -/
+private partial def depClosure (env : Environment) (seeds : List Name)
+    : List (Name × ConstantInfo) := Id.run do
+  let mut needed : Std.HashSet Name := {}
+  let mut worklist := seeds
+  while !worklist.isEmpty do
+    match worklist with
+    | [] => break
+    | n :: rest =>
+      worklist := rest
+      if needed.contains n then continue
+      needed := needed.insert n
+      if let some ci := env.constants.find? n then
+        let mut refs : NameSet := ci.type.getUsedConstantsAsSet
+        match ci with
+        | .defnInfo v =>
+          for r in v.value.getUsedConstantsAsSet do refs := refs.insert r
+        | .thmInfo v =>
+          for r in v.value.getUsedConstantsAsSet do refs := refs.insert r
+        | .opaqueInfo v =>
+          for r in v.value.getUsedConstantsAsSet do refs := refs.insert r
+        | .inductInfo v =>
+          for ctorName in v.ctors do
+            refs := refs.insert ctorName
+            if let some ctorCi := env.constants.find? ctorName then
+              for r in ctorCi.type.getUsedConstantsAsSet do refs := refs.insert r
+          for mutName in v.all do
+            refs := refs.insert mutName
+        | .ctorInfo v =>
+          refs := refs.insert v.induct
+        | .recInfo v =>
+          for mutName in v.all do
+            refs := refs.insert mutName
+          for rule in v.rules do
+            for r in rule.rhs.getUsedConstantsAsSet do refs := refs.insert r
+        | _ => pure ()
+        for r in refs do
+          if !needed.contains r then
+            worklist := r :: worklist
+  env.constants.toList.filter fun (n, _) => needed.contains n
+
+/-- Path to the parity `.ixe`, compiling it from the seed closure if absent.
+`buildFile` first: the test suite only builds what `IxTests` needs, not the rest
+of `Ix.lean`'s closure (e.g. the benchmarks it also imports), and `getFileEnv`
+needs every olean present. Then it loads the env and hands the transitive seed
+closure to the same FFI compile step `ix compile` uses. A seed that no longer
+resolves is a hard error, not a skip. -/
+public def ensure : IO System.FilePath := do
+  let out : System.FilePath := "tc-parity.ixe"
+  if ← out.pathExists then return out
+  let constsFile := ".github/fixtures/tc-parity-consts.txt"
+  IO.println s!"tc-parity: {out} not found — compiling from {constsFile}"
+  buildFile "Ix.lean"
+  let leanEnv ← getFileEnv "Ix.lean"
+  let raw ← Ix.Cli.ConstsFile.read constsFile
+  let mut seeds : List Name := []
+  for s in raw do
+    let name := s.toName
+    if leanEnv.constants.contains name then
+      seeds := name :: seeds
+    else
+      throw <| IO.userError s!"tc-parity: seed constant not found in Ix.lean env: {s}"
+  let closed := depClosure leanEnv seeds
+  let _ ← Ix.CompileM.rsCompileEnvBytesFFI closed out.toString
+  return out
+
+end Tests.Tc.ParityEnv
diff --git a/Tests/Ix/Tc/Pins.lean b/Tests/Ix/Tc/Pins.lean
index ac3ed5d1..554b76ce 100644
--- a/Tests/Ix/Tc/Pins.lean
+++ b/Tests/Ix/Tc/Pins.lean
@@ -3,18 +3,18 @@ module
 public import LSpec
 public import Ix.Tc
 public import Ix.Cli.CheckLeanCmd
+public import Tests.Ix.Tc.ParityEnv
 
 /-!
 `tc-pins` (ignored runner): regression pins for the pure-Lean kernel
-against a real serialized env (`IX_PINS_IXE`, e.g. `compileinitstd.ixe`).
+against a real serialized env (compiled on demand — see `Tests.Tc.ParityEnv`).
 Each pin is a constant that previously OOMed, was falsely rejected at
 depth 2001, or blew the worker stack (see the short-circuit note in
 `Ix/Tc/DefEq.lean` and `ParCheckCfg.stackBytes`); the suite ingresses
 the env once and checks each pin subject-only under a wall-clock budget.
 Budgets are generous — the pins guard ∞/OOM regression classes, not
-micro-perf. Skips (passing) when `IX_PINS_IXE` is unset so `--ignored`
-sweeps don't require the env file; known-slow pins (open perf issues)
-run only with `IX_PINS_SLOW=1`.
+micro-perf. Known-slow pins (open perf issues) run only with
+`IX_PINS_SLOW=1`.
 -/
 
 namespace Tests.Tc.Pins
@@ -74,14 +74,8 @@ def checkPin (kenv : MetaEnv) (prims : Primitives .meta)
 
 public def run : IO UInt32 := do
   IO.println "tc-pins"
-  let some path ← IO.getEnv "IX_PINS_IXE"
-    | IO.println "tc-pins: IX_PINS_IXE unset — skipping (point it at a \
-                  compileinitstd-style .ixe to run the pins)"
-      return 0
+  let path ← Tests.Tc.ParityEnv.ensure
   let includeSlow := (← IO.getEnv "IX_PINS_SLOW").isSome
-  if !(← System.FilePath.pathExists path) then
-    IO.eprintln s!"tc-pins: IX_PINS_IXE file not found: {path}"
-    return 1
   let t0 ← IO.monoMsNow
   let bytes ← IO.FS.readBinFile path
   match Ixon.deEnv bytes with
diff --git a/Tests/Main.lean b/Tests/Main.lean
index aca8a3f5..8525fa00 100644
--- a/Tests/Main.lean
+++ b/Tests/Main.lean
@@ -224,11 +224,11 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
   -- lean4lean dependency smoke: accept a real closure, reject an
   -- ill-typed decl (see Tests.Ix.Lean4Lean).
   ("lean4lean", Tests.Ix.Lean4Lean.run env),
-  -- Pure-Lean kernel regression pins against a real .ixe (needs
-  -- IX_PINS_IXE; skips cleanly otherwise — see Tests.Tc.Pins).
+  -- Pure-Lean kernel regression pins against a real .ixe, compiled on
+  -- demand (see Tests.Tc.ParityEnv).
   ("tc-pins", Tests.Tc.Pins.run),
-  -- Accelerated-vs-pure reduction differentials (IX_PINS_IXE-gated;
-  -- see Tests.Tc.AccelDiff and TcState.noAccel).
+  -- Accelerated-vs-pure reduction differentials over that same real env
+  -- (see Tests.Tc.AccelDiff and TcState.noAccel).
   ("tc-accel-diff", Tests.Tc.AccelDiff.run),
 ]
 
@@ -250,7 +250,14 @@ def main (args : List String) : IO UInt32 := do
 
   let runIgnored := args.contains "--ignored"
   let includeIgnored := args.contains "--include-ignored"
-  let filterArgs := args.filter fun a => a != "--ignored" && a != "--include-ignored"
+  -- `--exclude=a,b,c` drops the named ignored suites/runners from the sweep, so
+  -- one job can run every ignored test except the suites another job owns.
+  let excludeSet : List String :=
+    match args.find? (·.startsWith "--exclude=") with
+    | some a => (a.drop ("--exclude=".length)).toString.splitOn "," |>.filter fun s => !s.isEmpty
+    | none => []
+  let filterArgs := args.filter fun a =>
+    a != "--ignored" && a != "--include-ignored" && !a.startsWith "--exclude="
 
   -- Run primary tests unless --ignored (without --include-ignored) is specified
   if !runIgnored || includeIgnored then
@@ -264,20 +271,22 @@ def main (args : List String) : IO UInt32 := do
 
   -- Run ignored tests when --ignored or --include-ignored is specified
   if runIgnored || includeIgnored then
-    let mut result ← LSpec.lspecIO ignoredSuites filterArgs
     let env ← get_env!
-    let ignored := ignoredRunners env
-    -- A filter arg matching no runner must be an ERROR, not a silent
-    -- no-op: `filterMap` would drop it, leaving nothing to run and
-    -- returning 0, so a typo'd suite name reports success having
-    -- executed nothing.
-    for arg in filterArgs do
-      if !(ignored.any fun (key, _) => key == arg)
+    let allRunners := ignoredRunners env
+    -- A named suite — selected via a filter arg or removed via `--exclude` —
+    -- that matches nothing is an ERROR, not a silent no-op: otherwise a typo
+    -- runs (or excludes) nothing and still reports success having executed
+    -- nothing.
+    for arg in filterArgs ++ excludeSet do
+      if !(allRunners.any fun (key, _) => key == arg)
           && !ignoredSuites.contains arg then
         IO.eprintln s!"error: no ignored suite or runner named '{arg}'"
         return 1
-    let filtered := if filterArgs.isEmpty then ignored
-      else filterArgs.filterMap fun arg => ignored.find? fun (key, _) => key == arg
+    let suites := excludeSet.foldl (fun m k => m.erase k) ignoredSuites
+    let runners := allRunners.filter fun (key, _) => !excludeSet.contains key
+    let mut result ← LSpec.lspecIO suites filterArgs
+    let filtered := if filterArgs.isEmpty then runners
+      else filterArgs.filterMap fun arg => runners.find? fun (key, _) => key == arg
     for (_, action) in filtered do
       let r ← action
       if r != 0 then result := r