diff --git a/.github/scripts/check_sorry_frontier.pl b/.github/scripts/check_sorry_frontier.pl
deleted file mode 100755
index ab088d7..0000000
--- a/.github/scripts/check_sorry_frontier.pl
+++ /dev/null
@@ -1,267 +0,0 @@
-#!/usr/bin/env perl
-use strict;
-use warnings;
-
-# Enforce the checked-in Lean4Lean sorry frontier.
-#
-# This is a source-token audit rather than a raw grep: comments and strings
-# may discuss sorries without enlarging the trusted frontier. Every real
-# Lean sorry token is attributed to its nearest top-level declaration and
-# compared with the exact allowlist below. Progress = shrinking allowlist;
-# any new sorry (or a moved/renamed one) fails loudly.
-#
-# The allowlist is the gap inventory of the fork execution plan
-# (ix:plans/lean4lean-upstream-gaps.md §2), tiered:
-#   S - missing specification (nothing exists to prove against)
-#   P - stated but sorried, blocked only on Tier S
-#   V - upstream checker verification, blocked on Tiers S/P
-#   R - research-grade metatheory (open frontier, not scheduled)
-# Lean4Lean/Experimental/ is excluded from the scan entirely: parked or
-# abandoned proof attacks, not part of the trusted development.
-#
-# Usage: check_sorry_frontier.pl [repo-root]   (defaults to script's ../..)
-
-use Cwd qw(abs_path);
-use FindBin qw($RealBin);
-use File::Find qw(find);
-use File::Spec;
-
-my $repo_root =
-  @ARGV
-  ? abs_path($ARGV[0])
-  : abs_path(File::Spec->catdir($RealBin, '..', '..'));
-die "not a directory: $repo_root\n" unless -d $repo_root;
-
-my @exclude_prefixes = (
-  '.lake/',
-  'Lean4Lean/Experimental/',
-  'nix/',
-);
-
-my %expected = (
-  # Tier S - missing specification
-  # (VInductDecl.WF and VEnv.addInduct are real staged definitions)
-  "Lean4Lean/Verify/Typing/Expr.lean\0def TrProj"          => 1,
-  # Tier P - blocked only on Tier S
-  # (addInduct_WF proven for the stage-3 direct-indexed class, 2026-07-30)
-  "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.weak'"      => 1,
-  "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.weak'_inv"  => 1,
-  "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.defeqDFC"   => 1,
-  "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.wf"         => 1,
-  "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.uniq"       => 1,
-  "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.instN"      => 1,
-  "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.instL"      => 1,
-  # Tier V - checker verification, blocked on Tiers S/P
-  "Lean4Lean/Verify/Level.lean\0NormLevel.subsumption_eval"     => 1,
-  "Lean4Lean/Verify/Level.lean\0isEquiv_wf"                    => 1,
-  "Lean4Lean/Verify/Environment.lean\0addDecl.WF"              => 1,
-  "Lean4Lean/Verify/TypeChecker/InferType.lean\0inferProj.WF"   => 1,
-  "Lean4Lean/Verify/TypeChecker/WHNF.lean\0reduceRecursor.WF"   => 1,
-  "Lean4Lean/Verify/TypeChecker/WHNF.lean\0reduceProj.WF"       => 1,
-  "Lean4Lean/Verify/TypeChecker/IsDefEq.lean\0tryEtaStructCore.WF" => 1,
-  "Lean4Lean/Verify/TypeChecker/IsDefEq.lean\0isDefEqUnitLike.WF"  => 1,
-  # Tier R - research-grade metatheory (do not schedule; upstream-driven)
-  "Lean4Lean/Theory/Typing/Injectivity.lean\0IsDefEqU.sort_inv" => 1,
-  "Lean4Lean/Theory/Typing/Injectivity.lean\0IsDefEqU.forallE_inv_stratified" => 1,
-  "Lean4Lean/Theory/Typing/Injectivity.lean\0IsDefEqU.sort_forallE_inv" => 1,
-  "Lean4Lean/Theory/Typing/UniqueTyping.lean\0IsDefEqU.weakN_iff"   => 1,
-  "Lean4Lean/Theory/Typing/ChurchRosser.lean\0NormalEq.parRed"      => 2,
-);
-
-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]*(?:@\[[^\]]*\][ \t]+)*
-        (?:(?:private|protected|noncomputable|nonrec)[ \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 @lean_files;
-  find(
-    {
-      no_chdir => 1,
-      wanted => sub {
-        return unless -f $File::Find::name;
-        return unless $File::Find::name =~ /\.lean\z/;
-        my $relative = relative_path($File::Find::name);
-        for my $prefix (@exclude_prefixes) {
-          return if index($relative, $prefix) == 0;
-        }
-        push @lean_files, $File::Find::name;
-      },
-    },
-    $repo_root,
-  );
-  for my $path (sort @lean_files) {
-    push @observed_with_lines, find_sorries($path);
-  }
-  1;
-} or do {
-  my $error = $@ || 'unknown scan error';
-  print STDERR "sorry-frontier 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 "Lean4Lean 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 trusted frontier intentionally changes.\n";
-  exit 1;
-}
-
-print "Lean4Lean sorry frontier OK (" . scalar(@observed_with_lines) . " known sorries):\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 b5578df..6802494 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -2,19 +2,20 @@ name: CI
 
 on:
   push:
-    branches: [master]
+    branches: [dev]
   pull_request:
   workflow_dispatch:
 
-# A newer push to the same branch supersedes an in-flight run; master runs are
-# never cancelled, since those are the ones that populate the build cache.
+permissions:
+  contents: read
+
 concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: ${{ github.ref != 'refs/heads/master' }}
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
 
 jobs:
   build:
-    name: Build and self-check
+    name: Build and test
     runs-on: ubuntu-latest
     timeout-minutes: 60
     steps:
@@ -35,6 +36,15 @@ jobs:
       - name: Build Lean4Lean.Experimental
         run: lake build Lean4Lean.Experimental
 
+      # Enforce the trusted sorry frontier: fail if any `Theory`/`Verify`
+      # declaration gains, loses, or renames a `sorry` versus the allowlist in
+      # `Lean4Lean/Audit/SorryFrontier.lean`. Asks the compiled environment which
+      # declarations use `sorryAx`, so it can't drift over comments or string
+      # literals the way a source grep can. Not a default target, so it is built
+      # explicitly here; the surface it imports is already built above.
+      - name: Check sorry frontier
+        run: lake build Lean4Lean.Audit.SorryFrontier
+
       # `lake build` only establishes that lean4lean compiles; these check that it still
       # *works*. The two modes exercise different code paths, so both are worth running.
 
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index f643892..8b88f7b 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -2,7 +2,7 @@ name: Nix
 
 on:
   push:
-    branches: [master]
+    branches: [dev]
   pull_request:
   workflow_dispatch:
 
@@ -14,50 +14,43 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  # Cheap gates first: formatting and whole-flake evaluation for every
-  # declared system, without building anything.
-  eval:
-    runs-on: ubuntu-latest
+  # Packaging-compatibility gate: build the shipped outputs and every flake
+  # check on x86_64-linux (the only supported system). ci.yml is the primary
+  # lean-action build and test. The other systems in flake.nix stay declared
+  # but are not built here, so they never gate CI.
+  nix-test:
+    name: Nix Tests
+    runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v7
-      - name: Sorry frontier
-        run: perl .github/scripts/check_sorry_frontier.pl
-      - uses: DeterminateSystems/nix-installer-action@v20
-      - name: Check formatting
-        run: nix fmt --accept-flake-config -- --check flake.nix
-      - name: Evaluate all systems
-        run: nix flake check --all-systems --no-build --accept-flake-config
-
-  # Build the shipped outputs and run every check (proofs, the
-  # downstream-consumer fixture, and the CLI smoke/no-arg regression
-  # tests) on Linux.
-  check-linux:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v7
-      - uses: DeterminateSystems/nix-installer-action@v20
-      - uses: cachix/cachix-action@v16
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - uses: cachix/cachix-action@v17
         with:
           name: argumentcomputer
           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-          # Only push from trusted master builds; PRs stay read-only.
-          skipPush: ${{ github.ref != 'refs/heads/master' }}
-      - name: Build packages
-        run: nix build --accept-flake-config --no-link --print-build-logs .#lake-dependency .#lake-dependency-full .#lean4lean
-      - name: Flake checks
-        run: nix flake check --accept-flake-config --print-build-logs
+      - name: Check formatting
+        run: nix fmt --accept-flake-config -- --check flake.nix
+      # Shipped outputs: the CLI and the downstream Lake-dependency artifact.
+      - run: nix build --print-build-logs --accept-flake-config .#lean4lean .#lake-dependency
+      # Builds every check (proofs + sorry frontier, tests, consumer fixture,
+      # CLI regressions) and evaluates the rest of the flake.
+      - run: nix flake check --print-build-logs --accept-flake-config
 
-  # One Darwin runner exercising the wrapper and the consumer fixture,
-  # per the improvement plan; the full check matrix stays on Linux.
-  build-darwin:
-    runs-on: macos-latest
+  # Verify the dev shell provides a working Lake toolchain.
+  nix-devshell:
+    name: Nix devShell
+    runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v7
-      - uses: DeterminateSystems/nix-installer-action@v20
-      - uses: cachix/cachix-action@v16
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - uses: cachix/cachix-action@v17
         with:
           name: argumentcomputer
           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-          skipPush: ${{ github.ref != 'refs/heads/master' }}
-      - name: Build wrapper and consumer check
-        run: nix build --accept-flake-config --no-link --print-build-logs .#lean4lean .#checks.aarch64-darwin.downstream-consumer .#checks.aarch64-darwin.cli-smoke
+      - run: nix develop --accept-flake-config --command bash -c "lake build"
diff --git a/Lean4Lean/Audit/SorryFrontier.lean b/Lean4Lean/Audit/SorryFrontier.lean
new file mode 100644
index 0000000..f48b730
--- /dev/null
+++ b/Lean4Lean/Audit/SorryFrontier.lean
@@ -0,0 +1,131 @@
+import Lean4Lean.Theory
+import Lean4Lean.Theory.InductiveFixtures
+import Lean4Lean.Theory.Typing.Injectivity
+import Lean4Lean.Verify
+import Lean4Lean.Verify.Level
+import Lean4Lean.Verify.Environment
+import Lean4Lean.Verify.Environment.IndexedVecCandidate
+import Lean4Lean.Verify.Environment.IndexedVecConsReplay
+import Lean4Lean.Verify.Environment.IndexedVecConstructors
+import Lean4Lean.Verify.Environment.IndexedVecOuterReplay
+import Lean4Lean.Verify.Environment.IndexedVecSemanticReplay
+import Lean4Lean.Verify.Environment.InductiveFixtures
+import Lean4Lean.Verify.Environment.Normalization
+import Lean4Lean.Verify.TypeChecker.InferType
+import Lean4Lean.Verify.TypeChecker.WHNF
+import Lean4Lean.Verify.TypeChecker.IsDefEq
+
+/-!
+# Lean4Lean sorry frontier
+
+Guards the trusted verification frontier: the exact set of `Lean4Lean.Theory.*`
+and `Lean4Lean.Verify.*` declarations that are allowed to depend on `sorry`.
+Progress shrinks the allowlist; a new, moved, or renamed sorry fails the build.
+
+Unlike a source-token grep, this asks the compiled environment which
+declarations directly reference `sorryAx` (the elaborated form of a `sorry`
+token), so it can never drift from Lean's lexer over comments, string/char
+literals, or nested block comments. Attribution is by SOURCE MODULE via
+`getModuleIdxFor?`, so a declaration is charged to the file that defines it even
+when it sits in a foreign namespace (e.g. `Lean.Level.isEquiv_wf` lives in
+`Lean4Lean.Verify.Level`).
+
+The audited surface is exactly the modules reachable from this file's imports:
+importing a `Theory`/`Verify` module here is what brings it into scope. A sorry
+in a proof module not (transitively) imported here is not seen, so when a new
+`Theory`/`Verify` file joins the trusted build, add its import below.
+`Lean4Lean.Experimental.*` is parked proof work outside the trusted surface and
+is intentionally not imported.
+
+Runs as a build-time `run_cmd`, not an executable: `lake build` of this module
+is the whole check.
+-/
+
+open Lean Lean.Elab.Command
+
+namespace Lean4Lean.Audit
+
+/-- Constants referenced directly by a declaration's type or value, following
+the cases of `Lean.collectAxioms`. The `Lean.` qualifiers are load-bearing:
+this file imports lean4lean's kernel, which defines its own `Name`/
+`ConstantInfo` that would otherwise shadow Lean's inside this namespace. -/
+private def directConstants : 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
+
+/-- Prefixes whose modules make up the audited verification surface. -/
+private def surfacePrefixes : Array Lean.Name := #[`Lean4Lean.Theory, `Lean4Lean.Verify]
+
+/-- The checked-in sorry frontier, tiered as in the fork's upstream-gaps plan:
+S (missing specification), P (stated but sorried, blocked on S), V (checker
+verification, blocked on S/P), R (research-grade metatheory, upstream-driven). -/
+private def allowlist : Array Lean.Name := #[
+  -- Tier S — missing specification
+  `Lean4Lean.TrProj,
+  -- Tier P — blocked only on Tier S
+  `Lean4Lean.TrProj.weak',
+  `Lean4Lean.TrProj.weak'_inv,
+  `Lean4Lean.TrProj.defeqDFC,
+  `Lean4Lean.TrProj.wf,
+  `Lean4Lean.TrProj.uniq,
+  `Lean4Lean.TrProj.instN,
+  `Lean4Lean.TrProj.instL,
+  -- Tier V — checker verification, blocked on Tiers S/P
+  `Lean.Level.Normalize.NormLevel.subsumption_eval,
+  `Lean.Level.isEquiv_wf,
+  `Lean4Lean.addDecl.WF,
+  `Lean4Lean.TypeChecker.Inner.inferProj.WF,
+  `Lean4Lean.TypeChecker.Inner.reduceRecursor.WF,
+  `Lean4Lean.TypeChecker.Inner.reduceProj.WF,
+  `Lean4Lean.TypeChecker.Inner.tryEtaStructCore.WF,
+  `Lean4Lean.TypeChecker.Inner.isDefEqUnitLike.WF,
+  -- Tier R — research-grade metatheory (upstream-driven, not scheduled)
+  `Lean4Lean.VEnv.IsDefEqU.sort_inv,
+  `Lean4Lean.VEnv.IsDefEqU.forallE_inv_stratified,
+  `Lean4Lean.VEnv.IsDefEqU.sort_forallE_inv,
+  `Lean4Lean.VEnv.IsDefEqU.weakN_iff,
+  `Lean4Lean.VEnv.NormalEq.parRed,
+  -- Tier F — deliberately kernel-rejected inductive fixtures. Elaborator error
+  -- recovery admits the invalid `inductive` with `sorryAx`, so the constant
+  -- carries a sorry dependency even though the source has no `sorry` token
+  -- (which is why the old source-token scan never saw these). Not proof debt.
+  `Lean4Lean.InductiveFixtures.KernelDifferential.KernelRejectRecDomain,
+  `Lean4Lean.InductiveFixtures.KernelDifferential.KernelRejectRecIndex]
+
+/-- Declarations in the audited surface that directly reference `sorryAx`. -/
+private def observedFrontier (env : Lean.Environment) : Array Lean.Name := Id.run do
+  let moduleNames := env.allImportedModuleNames
+  let mut observed := #[]
+  for (name, info) in env.constants.toList do
+    if let some idx := env.getModuleIdxFor? name then
+      let mod := moduleNames[idx.toNat]!
+      if surfacePrefixes.any (·.isPrefixOf mod) && (directConstants info).contains ``sorryAx then
+        observed := observed.push name
+  return observed
+
+run_cmd do
+  let env ← getEnv
+  let observed := observedFrontier env
+  let expected : Std.HashSet Lean.Name := allowlist.foldl (·.insert ·) {}
+  let observedSet : Std.HashSet Lean.Name := observed.foldl (·.insert ·) {}
+  let added := observed.filter (!expected.contains ·) |>.qsort Name.lt
+  let removed := allowlist.filter (!observedSet.contains ·) |>.qsort Name.lt
+  if added.isEmpty && removed.isEmpty then
+    logInfo m!"Lean4Lean sorry frontier OK ({observed.size} known sorries)"
+  else
+    let fmt (hdr : String) (ns : Array Name) : String :=
+      if ns.isEmpty then "" else
+        s!"\n{hdr}\n" ++ String.intercalate "\n" (ns.toList.map (s!"  {·}"))
+    throwError m!"Lean4Lean sorry frontier changed.\
+      {fmt "New sorries (not in allowlist):" added}\
+      {fmt "Expected sorries now absent (update the allowlist):" removed}\n\
+      Edit the allowlist in Lean4Lean/Audit/SorryFrontier.lean only when the \
+      trusted frontier intentionally changes."
+
+end Lean4Lean.Audit
diff --git a/flake.nix b/flake.nix
index 16cd2d7..77daa82 100644
--- a/flake.nix
+++ b/flake.nix
@@ -44,10 +44,24 @@
       }: let
         # Lake package
         lake2nix = pkgs.callPackage lean4-nix.lake {};
-        # lean4-nix reads lake-manifest.json while evaluating derivations.
-        # Reuse the flake's lazy source instead of creating a nested
-        # fileset.toSource path that may be unrealized under --no-build.
-        leanSrc = inputs.self.outPath;
+        # Restrict the Lake build inputs to Lean-relevant files so edits to
+        # unrelated files (CI, docs, the flake itself) don't invalidate the
+        # cached Lean derivations. Covers the library/CLI/proof/test/audit
+        # sources, the manifests lean4-nix reads while evaluating, and the
+        # downstream-consumer fixture built from `${leanSrc}/nix/fixtures`.
+        # NOTE: a fileset source is left unrealized under `nix flake check
+        # --no-build` (fails with "path '…-source' is not valid"), so the nix
+        # CI job builds for real rather than eval-only.
+        leanSrc = pkgs.lib.fileset.toSource {
+          root = ./.;
+          fileset = pkgs.lib.fileset.unions [
+            ./lakefile.toml
+            ./lake-manifest.json
+            ./lean-toolchain
+            ./nix/fixtures
+            (pkgs.lib.fileset.fileFilter (f: f.hasExt "lean") ./.)
+          ];
+        };
         # Batteries v4.31.0 accidentally split deprecated recycling modules
         # into a second Lake library with a dependency back to Batteries.  Its
         # shared/static facets therefore form a cycle, which matters here
@@ -64,14 +78,16 @@
           src = leanSrc;
           depOverride.batteries.patches = [batteries431CycleFix];
         };
+        # System inputs every Lake build/derivation here needs.
+        leanBuildInputs = [
+          pkgs.gmp
+          pkgs.lean.lean-all
+          pkgs.rsync
+        ];
         lakeBuildArgs = {
           inherit lakeDeps;
           src = leanSrc;
-          buildInputs = [
-            pkgs.gmp
-            pkgs.lean.lean-all
-            pkgs.rsync
-          ];
+          buildInputs = leanBuildInputs;
         };
 
         # The Lake dependency artifact: the contract consumed by downstream
@@ -82,7 +98,7 @@
         # link executables against this read-only store path. No CLI, no
         # proof targets. (lean4-nix's capitalization heuristic would guess
         # the nonexistent `Lean4lean` target, hence the explicit name.)
-        lean4leanLakeDependency = lake2nix.mkPackage (
+        lean4leanLib = lake2nix.mkPackage (
           lakeBuildArgs
           // {
             name = "Lean4Lean";
@@ -93,44 +109,25 @@
           }
         );
 
-        # Like lake-dependency, but additionally builds the Theory and
-        # Verify proof libraries (default facets), for consumers that
-        # import the metatheory too — Ix's IxTcVerify imports both
-        # Lean4Lean.Theory.* and Lean4Lean.Verify.*, so the plain
-        # implementation-only artifact is not enough for it.
-        lean4leanLakeDependencyFull = lake2nix.mkPackage (
-          lakeBuildArgs
-          // {
-            name = "Lean4Lean-full";
-            lakeArtifacts = lean4leanLakeDependency;
-            buildPhase = ''
-              runHook preBuild
-              lake build Lean4Lean Lean4Lean.Theory Lean4Lean.Verify
-              lake build Lean4Lean:shared Lean4Lean:static
-              runHook postBuild
-            '';
-            meta = {
-              description = "Lean4Lean library artifact including the Theory and Verify proof libraries";
-            };
-          }
-        );
+        # Common mkPackage args that reuse the prebuilt library artifact as the
+        # Lake build's starting point and skip re-installing it — for the CLI
+        # and checks, which extend the library but don't ship it.
+        reuseLibArgs = {
+          lakeArtifacts = lean4leanLib;
+          installArtifacts = false;
+        };
 
         # Search path covering the library and its Lake deps (batteries).
         leanPath = pkgs.lib.concatStringsSep ":" (
           map (d: "${d}/.lake/build/lib/lean") (
-            [lean4leanLakeDependency] ++ builtins.attrValues lakeDeps
+            [lean4leanLib] ++ builtins.attrValues lakeDeps
           )
         );
 
         # Raw CLI build: reuses the dependency artifact and keeps only
         # bin/lean4lean (no source copy, IR, or duplicate executable).
         lean4leanCLIRaw = lake2nix.mkPackage (
-          lakeBuildArgs
-          // {
-            lakeArtifacts = lean4leanLakeDependency;
-            installArtifacts = false;
-            name = "lean4lean";
-          }
+          lakeBuildArgs // reuseLibArgs // {name = "lean4lean";}
         );
 
         # Wrapped CLI:
@@ -158,22 +155,40 @@
               --prefix LEAN_PATH : "${leanPath}"
           '';
 
+        # A check that builds extra Lake targets over the library artifact and
+        # installs nothing: the build — including any elaboration-time
+        # assertions in those targets — is the test.
+        mkLakeCheck = name: buildTargets:
+          lake2nix.mkPackage (
+            lakeBuildArgs
+            // reuseLibArgs
+            // {
+              inherit name;
+              buildPhase = ''
+                runHook preBuild
+                ${buildTargets}
+                runHook postBuild
+              '';
+            }
+          );
+
         # Proof libraries: the abstract metatheory and the proof that the
-        # implementation satisfies it. One derivation builds both targets
-        # in one Lake workspace so Theory modules are compiled once.
-        proofs = lake2nix.mkPackage (
-          lakeBuildArgs
-          // {
-            name = "Lean4Lean-proofs";
-            lakeArtifacts = lean4leanLakeDependency;
-            installArtifacts = false;
-            buildPhase = ''
-              runHook preBuild
-              lake build Lean4Lean.Theory Lean4Lean.Verify
-              runHook postBuild
-            '';
-          }
-        );
+        # implementation satisfies it, built in one Lake workspace so Theory
+        # modules compile once, then the sorry frontier:
+        # `Lean4Lean.Audit.SorryFrontier` fails the build if any Theory/Verify
+        # declaration gains, loses, or renames a `sorry` versus its allowlist.
+        # It is not a default target, so building it over the just-built
+        # surface is the whole check.
+        proofs = mkLakeCheck "Lean4Lean-proofs" ''
+          lake build Lean4Lean.Theory Lean4Lean.Verify
+          lake build Lean4Lean.Audit.SorryFrontier
+        '';
+
+        # Basic test suite: the `Lean4Lean.Tests.*` regression modules (the
+        # nested-inductive kernel checks and the toolchain audit) run their
+        # assertions at elaboration via `run_meta`/`#guard`, so building the
+        # target is the test run.
+        tests = mkLakeCheck "Lean4Lean-tests" "lake build Lean4Lean.Tests";
 
         # Downstream-consumer check: a minimal Lake package that requires
         # lean4lean, links an executable against the read-only dependency
@@ -183,75 +198,57 @@
         # fails before any consumer updates its pin.
         consumer = lake2nix.mkPackage {
           name = "consumer";
-          # lake2nix reads this fixture's manifest during evaluation. Keep it
-          # inside the already-realized flake source rather than coercing the
-          # subdirectory into a second, not-yet-realized store path.
+          # lake2nix reads this fixture's manifest during evaluation; it is
+          # included in `leanSrc` (the fileset covers `nix/fixtures`), so it is
+          # taken from the library's source path rather than a separate store
+          # path.
           src = "${leanSrc}/nix/fixtures/consumer";
           lakeDeps = {
-            lean4lean = lean4leanLakeDependency;
+            lean4lean = lean4leanLib;
             batteries = lakeDeps.batteries;
           };
           installArtifacts = false;
-          buildInputs = [
-            pkgs.gmp
-            pkgs.lean.lean-all
-            pkgs.rsync
-          ];
+          buildInputs = leanBuildInputs;
           postBuild = ''
             ./.lake/build/bin/consumer | grep -q consumer-ok
           '';
         };
 
-        # Regression test for the `replayFromImports` teardown segfault (see
-        # plans/DEPRECATED-segfault-fix-plan.md): run the shipped wrapper from a clean
-        # environment on a small module and require a clean exit plus the
-        # summary line the crash used to swallow.
-        cliSmoke =
-          pkgs.runCommand "lean4lean-cli-smoke" {}
-          ''
-            unset LEAN_PATH LEAN_SYSROOT
-            ${lean4leanCLI}/bin/lean4lean Lean4Lean.Declaration > out
+        # A CLI check: run `body` (which writes the wrapped CLI's stdout to
+        # `out`), then require the "checked N declarations" summary line.
+        mkCliCheck = name: body:
+          pkgs.runCommand "lean4lean-${name}" {} ''
+            ${body}
             grep -Eq "^checked [0-9]+ declarations" out
             touch $out
           '';
 
+        # Regression test for the `replayFromImports` teardown segfault (see
+        # plans/DEPRECATED-segfault-fix-plan.md): run the shipped wrapper from a
+        # clean environment on a small module and require a clean exit plus the
+        # summary line the crash used to swallow.
+        cliSmoke = mkCliCheck "cli-smoke" ''
+          unset LEAN_PATH LEAN_SYSROOT
+          ${lean4leanCLI}/bin/lean4lean Lean4Lean.Declaration > out
+        '';
+
         # The external-project case: with an ambient LEAN_PATH already set
         # (as `lake env` sets one for a target project), the wrapper must
         # prepend its package paths rather than lose them or clobber the
         # ambient value — a --set/--set-default wrapper fails this check.
-        cliSmokeExternal =
-          pkgs.runCommand "lean4lean-cli-smoke-external" {}
-          ''
-            mkdir ambient
-            LEAN_PATH=$PWD/ambient ${lean4leanCLI}/bin/lean4lean Lean4Lean.Declaration > out
-            grep -Eq "^checked [0-9]+ declarations" out
-            touch $out
-          '';
+        cliSmokeExternal = mkCliCheck "cli-smoke-external" ''
+          mkdir ambient
+          LEAN_PATH=$PWD/ambient ${lean4leanCLI}/bin/lean4lean Lean4Lean.Declaration > out
+        '';
 
         # No-argument mode: with only the repo's lake-manifest.json in the
         # working directory, the CLI must infer the package (matching the
         # manifest name case-insensitively against the Lean4Lean module
         # root) and check the whole library.
-        cliNoArg =
-          pkgs.runCommand "lean4lean-cli-noarg" {}
-          ''
-            cp ${./lake-manifest.json} lake-manifest.json
-            ${lean4leanCLI}/bin/lean4lean > out
-            grep -Eq "^checked [0-9]+ declarations" out
-            touch $out
-          '';
-        # Sorry-frontier audit: every real `sorry` token outside
-        # Lean4Lean/Experimental/ must match the script's exact allowlist
-        # (the upstream-gaps plan's Tier S/P/V/R inventory), so progress
-        # shrinks the allowlist and regressions fail loudly. Pure text
-        # audit — no Lean toolchain involved.
-        sorryFrontier =
-          pkgs.runCommand "lean4lean-sorry-frontier" {}
-          ''
-            ${pkgs.perl}/bin/perl \
-              ${./.github/scripts/check_sorry_frontier.pl} ${leanSrc} \
-              | tee $out
-          '';
+        cliNoArg = mkCliCheck "cli-noarg" ''
+          cp ${./lake-manifest.json} lake-manifest.json
+          ${lean4leanCLI}/bin/lean4lean > out
+        '';
       in {
         # Lean overlay
         _module.args.pkgs = import nixpkgs {
@@ -264,10 +261,7 @@
         packages = {
           default = lean4leanCLI;
           lean4lean = lean4leanCLI;
-          lake-dependency = lean4leanLakeDependency;
-          lake-dependency-full = lean4leanLakeDependencyFull;
-          # Compatibility alias for early users of the staged flake.
-          lib = lean4leanLakeDependency;
+          lake-dependency = lean4leanLib;
         };
 
         apps = let
@@ -282,8 +276,7 @@
         };
 
         checks = {
-          inherit proofs;
-          sorry-frontier = sorryFrontier;
+          inherit proofs tests;
           downstream-consumer = consumer;
           cli-smoke = cliSmoke;
           cli-smoke-external = cliSmokeExternal;