diff --git a/.github/actionlint.yaml b/.github/actionlint.yaml
new file mode 100644
index 0000000..44dc817
--- /dev/null
+++ b/.github/actionlint.yaml
@@ -0,0 +1,7 @@
+# Namespace runner labels used by the `lake-check-namespace` functional test. `lake check`
+# sandboxes with bubblewrap, which needs a privileged container on Namespace; the
+# `-with-features` suffix is what makes the feature label apply.
+self-hosted-runner:
+  labels:
+    - nscloud-ubuntu-24.04-amd64-2x4-with-features
+    - namespace-features:container.privileged=true
diff --git a/.github/functional_tests/lake_check/action.yml b/.github/functional_tests/lake_check/action.yml
new file mode 100644
index 0000000..94db6e0
--- /dev/null
+++ b/.github/functional_tests/lake_check/action.yml
@@ -0,0 +1,60 @@
+name: 'lake check test'
+description: 'Verify `lake-check: paranoid` succeeds on a clean package and fails once a sorry is introduced.'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
+runs:
+  using: 'composite'
+  steps:
+    # TODO: once `lean-action` supports just setup, use it here
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create a clean lake library
+      run: |
+        lake init foo lib
+        lake update
+      shell: bash
+
+    - name: "run `lean-action` (clean package)"
+      id: lean-action-clean
+      uses: ./
+      with:
+        use-github-cache: false
+        lake-check: paranoid
+
+    - name: verify lake check success on the clean package
+      env:
+        OUTPUT_NAME: "lake-check-status"
+        EXPECTED_VALUE: "SUCCESS"
+        ACTUAL_VALUE: ${{ steps.lean-action-clean.outputs.lake-check-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    # `lake check` permits only the standard axioms, so a `sorry` is enough to make every kernel
+    # it runs reject the project.
+    - name: introduce a sorry
+      run: |
+        printf '\ntheorem fooSorry : True := by sorry\n' >> Foo/Basic.lean
+      shell: bash
+
+    - name: "rerun `lean-action` (sorry introduced)"
+      id: lean-action-dirty
+      uses: ./
+      continue-on-error: true # required so that the failing check does not fail the workflow
+      with:
+        use-github-cache: false
+        lake-check: paranoid
+
+    - name: verify lake check failure once a sorry is introduced
+      env:
+        OUTPUT_NAME: "lake-check-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action-dirty.outputs.lake-check-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
diff --git a/.github/functional_tests/lake_check_unsupported/action.yml b/.github/functional_tests/lake_check_unsupported/action.yml
new file mode 100644
index 0000000..2b655ad
--- /dev/null
+++ b/.github/functional_tests/lake_check_unsupported/action.yml
@@ -0,0 +1,51 @@
+name: 'lake check unsupported toolchain test'
+description: 'Verify `lake-check` fails loudly, rather than silently passing, on a toolchain without `lake check`.'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test. Must be older than v4.35.0-rc1.'
+    required: true
+runs:
+  using: 'composite'
+  steps:
+    # TODO: once `lean-action` supports just setup, use it here
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create a clean lake library
+      run: |
+        lake init foo lib
+        lake update
+      shell: bash
+
+    - name: "run `lean-action` on a toolchain without `lake check`"
+      id: lean-action-unsupported
+      uses: ./
+      continue-on-error: true # required so that the expected failure does not fail the workflow
+      with:
+        use-github-cache: false
+        lake-check: "true"
+
+    # A check that cannot run has to be reported as a failure. Silently passing would tell a
+    # project its kernel was independently replayed when nothing ran at all.
+    - name: verify lake check fails on an unsupported toolchain
+      env:
+        OUTPUT_NAME: "lake-check-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action-unsupported.outputs.lake-check-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify the action step itself failed
+      env:
+        STEP_OUTCOME: ${{ steps.lean-action-unsupported.outcome }}
+      run: |
+        if [ "$STEP_OUTCOME" != "failure" ]; then
+          echo "::error::expected the lean-action step to fail, but its outcome was '$STEP_OUTCOME'"
+          exit 1
+        fi
+        echo "lean-action failed as expected"
+      shell: bash
diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml
index bb4480e..3deaa37 100644
--- a/.github/workflows/functional_tests.yml
+++ b/.github/workflows/functional_tests.yml
@@ -28,6 +28,9 @@ env:
   # Toolchain without the bundled `leanchecker` binary,
   # used to cover the external `lean4checker` fallback path
   legacy_toolchain: leanprover/lean4:v4.26.0
+  # `lake check --paranoid` landed in v4.35.0-rc2, which is newer than the toolchain pinned in
+  # `.github/functional_test_toolchain`, so the `lake-check` test pins its own.
+  lake_check_toolchain: leanprover/lean4:v4.35.0-rc2
 
 jobs:
   # The default toolchain is pinned in `.github/functional_test_toolchain`
@@ -243,6 +246,34 @@ jobs:
           # axiom-audit builds with the project's toolchain, so use a recent one.
           toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
+  # `lake check` sandboxes with bubblewrap, which GitHub-hosted runners do not permit without a
+  # privileged change to the runner. Namespace serves a privileged container, which permits it
+  # outright, so that is where this runs. The `-with-features` suffix is what makes the feature
+  # label apply. These labels are per-organisation configuration, and a job whose labels an
+  # organisation does not serve sits queued rather than failing, so keep this to the repository
+  # known to be provisioned for them.
+  lake-check-namespace:
+    if: github.repository == 'leanprover/lean-action'
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-2x4-with-features
+      - namespace-features:container.privileged=true
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+      - uses: ./.github/functional_tests/lake_check
+        with:
+          toolchain: ${{ env.lake_check_toolchain }}
+
+  # Pinned to a toolchain that predates `lake check`, rather than to the moving default: once the
+  # default supports it, this would otherwise quietly stop testing feature detection.
+  lake-check-unsupported-toolchain:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+      - uses: ./.github/functional_tests/lake_check_unsupported
+        with:
+          toolchain: ${{ env.legacy_toolchain }}
+
   macos-runner:
     needs: resolve-toolchain
     runs-on: macos-latest
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1c85943..e13acd9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Added
+
+- new `lake-check` input to check the project with `lake check`: build it and replay the result through one or more kernels inside a sandbox, erroring on any use of a non-standard axiom. `"true"` uses Lean's own kernel; `"paranoid"` additionally runs every external checker the toolchain bundles (`leanchecker-paranoid`, `lean4lean`, `nanoda`, `con-leche` and `con-ron`), none of which has to be built. Requires a Linux runner, Lean `v4.35.0-rc1` or newer (`"paranoid"` needs `v4.35.0-rc2`), and a runner permitting the user namespaces bubblewrap needs; see the README. Default: false
+- new `lake-check-status` output parameter
+
 ## v1.6.1 - 2026-10-02
 
 ### Changed
diff --git a/README.md b/README.md
index 9f6004f..7fed88b 100644
--- a/README.md
+++ b/README.md
@@ -90,6 +90,7 @@ If `lean-action` is unable to successfully run the step, `lean-action` will fail
 - `mk_all-check`
 - `check-reservoir-eligibility`
 - `leanchecker`
+- `lake-check`
 - `nanoda`
 
 ### Automatic configuration
@@ -226,6 +227,17 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Deprecated alias for `leanchecker`.
     lean4checker: ""
 
+    # Check the project with `lake check`: build it and replay the result through one or
+    # more kernels inside a sandbox, erroring on any use of a non-standard axiom.
+    # "true" checks with Lean's own kernel. "paranoid" additionally runs every external
+    # checker bundled with the toolchain: `leanchecker-paranoid`, `lean4lean`, `nanoda`,
+    # `con-leche` and `con-ron`. None of them has to be built.
+    # Requires a Linux runner, Lean `v4.35.0-rc1`+ ("paranoid" needs `v4.35.0-rc2`+), and a
+    # runner that permits the user namespaces bubblewrap needs.
+    # Allowed values: "true" | "false" | "paranoid".
+    # Default: "false"
+    lake-check: ""
+
     # Check environment with nanoda external type checker.
     # nanoda is an independent Lean 4 type checker written in Rust.
     # Requires Rust toolchain (will be installed automatically if not present).
@@ -286,6 +298,8 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
   - Values: "SUCCESS" | "FAILURE" | ""
 - `mk_all-status`
   - Values: "SUCCESS" | "FAILURE" | ""
+- `lake-check-status`
+  - Values: "SUCCESS" | "FAILURE" | ""
 - `nanoda-status`
   - Values: "SUCCESS" | "FAILURE" | ""
 - `axiom-audit-status`
@@ -374,6 +388,71 @@ Cap the parallelism by setting `LEAN_NUM_THREADS` on the `lean-action` step:
 
 Higher values trade memory for speed.
 
+## Independent kernel checks with `lake check`
+
+`lake check` builds the project, exports it, and replays the result through a kernel, erroring on
+any use of a non-standard axiom. It treats the project as untrusted input: the code is built and
+exported inside a sandbox, and none of its `.olean` files is loaded into Lake's own address space.
+The reference manual places this among the other ways to validate a proof, in
+[Validating a Lean Proof](https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-comparator).
+
+```yaml
+- uses: leanprover/lean-action@v1
+  with:
+    lake-check: "paranoid"
+```
+
+`lake-check: "true"` checks with Lean's own kernel. `lake-check: "paranoid"` additionally runs
+every external checker the toolchain bundles: `leanchecker-paranoid`, `lean4lean`, `nanoda`,
+`con-leche` and `con-ron`. Release toolchains ship all of them, so nothing is cloned or compiled.
+
+Only the standard axioms are permitted, so a project containing a `sorry` is rejected and there is
+no option to allow one.
+
+`lake check` builds the project itself, inside the sandbox. Whether it is *also* built on the
+runner first is the `build` input's business: leaving `build` on is faster, because `lake check`
+then starts from a populated `.lake`, while `build: false` keeps the project's code off the runner
+entirely. Note that the rest of `lean-action` runs project code on the runner, so the action as a
+whole does not give you `lake check`'s isolation; run `lake check` directly for genuinely
+adversarial input.
+
+### Making the sandbox able to start
+
+bubblewrap needs unprivileged user namespaces, and not every runner permits them.
+
+**GitHub-hosted runners** restrict them, so `lake-check` fails there until you grant them. The
+narrowest way is an AppArmor profile covering `bwrap` alone; the blunt way is to lift the
+restriction for the whole runner:
+
+```yaml
+- run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
+- uses: leanprover/lean-action@v1
+  with:
+    lake-check: "paranoid"
+```
+
+**Namespace runners** fail differently: jobs run in a container whose seccomp profile denies
+`pivot_root`, for root as well as for the job user, so relaxing user namespaces does not help.
+Request a privileged container instead, where the `-with-features` suffix on the machine label is
+what makes the feature apply:
+
+```yaml
+jobs:
+  verify:
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-8x16-with-features
+      - namespace-features:container.privileged=true
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-check: "paranoid"
+```
+
+Such a container permits user namespaces too, so nothing else is needed there. These labels are
+per-organisation configuration: a job whose labels your organisation does not serve sits queued
+rather than failing.
+
 ## Axiom Allowlist Audit with axiom-audit
 
 [axiom-audit](https://github.com/leanprover-community/axiom-audit) checks that every declaration in your library depends only on an allowlist of axioms (by default `propext`, `Classical.choice`, `Quot.sound`). Because it inspects the compiled kernel environment, it catches what a `grep` cannot: `sorry`/`admit` (`sorryAx`), `native_decide` (`Lean.ofReduceBool`), and any home-rolled `axiom`, including ones reaching in through imports.
diff --git a/action.yml b/action.yml
index b0bc7ed..bafa470 100644
--- a/action.yml
+++ b/action.yml
@@ -118,6 +118,19 @@ inputs:
       Allowed values: "true" | "false".
     required: false
     default: "false"
+  lake-check:
+    description: |
+      Check the project with `lake check`: build it and replay the result through one or more
+      kernels inside a sandbox, erroring on any use of a non-standard axiom.
+      "true" checks with Lean's own kernel. "paranoid" additionally runs every external checker
+      bundled with the toolchain: `leanchecker-paranoid`, `lean4lean`, `nanoda`, `con-leche` and
+      `con-ron`. None of them has to be built: release toolchains ship all of them.
+      Requires a Linux runner, Lean `v4.35.0-rc1` or newer ("paranoid" needs `v4.35.0-rc2`), and
+      a runner that permits the user namespaces bubblewrap needs. See the README for what that
+      takes on GitHub-hosted and Namespace runners.
+      Allowed values: "true" | "false" | "paranoid".
+    required: false
+    default: "false"
   nanoda:
     description: |
       Check environment with nanoda external type checker.
@@ -204,6 +217,11 @@ outputs:
       If lean-action detected a mathlib dependency equals "true"
       otherwise equals "false".
     value: ${{ steps.detect-mathlib.outputs.detected-mathlib }}
+  lake-check-status:
+    description: |
+      The status of the `lake check` step.
+      Allowed values: "SUCCESS" | "FAILURE" | "".
+    value: ${{ steps.lake-check.outputs.lake-check-status }}
   nanoda-status:
     description: |
       The status of the nanoda check step.
@@ -355,6 +373,17 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
+    - name: check the project with lake check
+      id: lake-check
+      if: ${{ inputs.lake-check != 'false' }}
+      env:
+        LAKE_CHECK_INPUT: ${{ inputs.lake-check }}
+      run: |
+        : Check the project with lake check
+        ${GITHUB_ACTION_PATH}/scripts/run_lake_check.sh
+      shell: bash
+      working-directory: ${{ inputs.lake-package-directory }}
+
     - name: check environment with nanoda
       id: nanoda
       if: ${{ inputs.nanoda == 'true' }}
diff --git a/scripts/run_lake_check.sh b/scripts/run_lake_check.sh
new file mode 100755
index 0000000..07a76e7
--- /dev/null
+++ b/scripts/run_lake_check.sh
@@ -0,0 +1,164 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Group logging using the ::group:: workflow command
+echo "::group::lake check Output"
+echo "Checking the project with \`lake check\`"
+
+# Set by the checks below when they can name the failure precisely; handle_exit falls back to a
+# generic message for anything that fails without setting one.
+failure_message=""
+
+# handle_exit captures the failing command's status, records the step output, and re-exits with
+# the same status.
+handle_exit() {
+    exit_status=$?
+    echo "::endgroup::"
+    if [ "$exit_status" -ne 0 ]; then
+        echo "lake-check-status=FAILURE" >> "$GITHUB_OUTPUT"
+        echo "::error::${failure_message:-lake check failed}"
+    else
+        echo "lake-check-status=SUCCESS" >> "$GITHUB_OUTPUT"
+    fi
+    exit "$exit_status"
+}
+trap handle_exit EXIT
+
+# The step guard in `action.yml` only runs this script when `lake-check` is not "false", so
+# anything other than the two running modes is a typo worth failing on rather than ignoring.
+mode="${LAKE_CHECK_INPUT:-}"
+case "$mode" in
+    true | paranoid) ;;
+    *)
+        failure_message="\`lake-check\` must be \"false\", \"true\" or \"paranoid\", got \"${mode}\""
+        exit 1
+        ;;
+esac
+
+# `lake check` sandboxes the code it checks with bubblewrap, which needs Linux namespaces; Lake
+# refuses to run anywhere else, so say so here rather than letting it fail further in.
+runner_os="$(uname -s)"
+if [ "$runner_os" != "Linux" ]; then
+    failure_message="\`lake-check\` requires a Linux runner: \`lake check\` sandboxes the code it checks with bubblewrap, which needs Linux namespaces. This runner is ${runner_os}."
+    exit 1
+fi
+
+# Feature-detect from the help text rather than comparing version strings: toolchains are often
+# nightlies or PR builds whose versions do not order usefully. A Lake without `lake check` prints
+# its top-level help here and still exits 0, so match on content, not on the exit status.
+check_help="$(lake check --help 2>&1 || true)"
+
+case "$check_help" in
+    *"Check this project against external checker(s)"*) ;;
+    *)
+        failure_message="\`lake-check\` needs \`lake check\`, which requires Lean v4.35.0-rc1 or newer."
+        exit 1
+        ;;
+esac
+
+if [ "$mode" = "paranoid" ]; then
+    case "$check_help" in
+        *"--paranoid"*) ;;
+        *)
+            failure_message="\`lake-check: paranoid\` needs \`lake check --paranoid\`, which requires Lean v4.35.0-rc2 or newer. This toolchain has \`lake check\`, so \`lake-check: true\` would work."
+            exit 1
+            ;;
+    esac
+fi
+
+# Resolve the same sandbox executable Lake will use. An explicit COMPARATOR_BWRAP that cannot be
+# run is an error rather than something to quietly paper over: Lake would still honour it, so
+# falling back to `bwrap` here would probe one executable and check with another.
+if [ -n "${COMPARATOR_BWRAP:-}" ]; then
+    if [ ! -x "${COMPARATOR_BWRAP}" ]; then
+        failure_message="COMPARATOR_BWRAP is set to \"${COMPARATOR_BWRAP}\", which is not an executable file. \`lake check\` would use it as its sandbox, so this is fatal rather than something to fall back from."
+        exit 2
+    fi
+    sandbox_exe="${COMPARATOR_BWRAP}"
+    echo "Using the sandbox at COMPARATOR_BWRAP=${sandbox_exe}"
+else
+    # The GitHub-hosted Ubuntu images do not ship bubblewrap, and neither do Namespace's.
+    if ! command -v bwrap > /dev/null 2>&1; then
+        echo "bubblewrap not found; installing it"
+        if ! command -v apt-get > /dev/null 2>&1; then
+            failure_message="\`lake-check\` needs \`bwrap\` on PATH, and \`apt-get\` is not available to install it. Install bubblewrap before calling lean-action, or point COMPARATOR_BWRAP at it."
+            exit 2
+        fi
+        sudo apt-get update
+        sudo apt-get install -y bubblewrap
+    fi
+    sandbox_exe="$(command -v bwrap)"
+fi
+
+# Probe the sandbox before running the check. An environment that cannot sandbox has to be
+# reported as a setup problem naming the remedy, not as a failed check: `lake check` exits 1 both
+# when it rejects a project and when bubblewrap fails to start, so by the time it has run the two
+# are hard to tell apart.
+sandbox_probe_output=""
+sandbox_works() {
+    sandbox_probe_output="$("$sandbox_exe" --ro-bind / / true 2>&1)"
+}
+
+if ! sandbox_works; then
+    # The remedy depends on which half of the sandbox was refused, so name the one that fits.
+    # A denied uid map means user namespaces are blocked; a denied `pivot_root` means the job is
+    # running inside a container, which is a different problem with a different fix.
+    case "$sandbox_probe_output" in
+        *"pivot_root"*)
+            hint="The user namespace was created but \`pivot_root\` was refused, which means this job is running in a container whose seccomp profile forbids it. On Namespace runners, request a privileged container: add \`namespace-features:container.privileged=true\` to \`runs-on\` and the \`-with-features\` suffix to the machine label. Otherwise use a runner that is not containerised."
+            ;;
+        *"uid map"* | *"user namespace"*)
+            hint="This runner restricts the unprivileged user namespaces bubblewrap needs, as GitHub-hosted runners do. Grant them before calling lean-action, either with an AppArmor profile permitting \`userns\` for ${sandbox_exe}, or with \`sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0\`. See \"Independent kernel checks with \\\`lake check\\\`\" in the lean-action README."
+            ;;
+        *)
+            hint="Make bubblewrap able to create its sandbox on this runner before calling lean-action."
+            ;;
+    esac
+    failure_message="\`lake check\` cannot start its sandbox, so nothing was checked: \`${sandbox_exe} --ro-bind / / true\` fails with \"${sandbox_probe_output}\". ${hint}"
+    exit 2
+fi
+echo "Sandbox check passed: bubblewrap can create a user namespace here"
+
+# `lake check` builds the project itself, inside the sandbox. Whether the project is also built on
+# the runner beforehand is the caller's choice, made with the `build` input: leaving it on is
+# faster because `lake check` then has a populated `.lake`, while turning it off keeps the
+# project's code off the runner entirely. Either way this script does not build it.
+
+# Keep a copy of the output: a sandbox that fails to start has to be told apart from a project
+# that was rejected, and `lake check` does not distinguish them by exit code.
+check_log="$(mktemp "${RUNNER_TEMP:-/tmp}/lake-check.XXXXXX")"
+
+status=0
+if [ "$mode" = "paranoid" ]; then
+    echo "Running \`lake check --paranoid\`: Lean's own kernel plus every bundled external checker"
+    lake check --paranoid 2>&1 | tee "$check_log" || status=$?
+else
+    echo "Running \`lake check\`"
+    lake check 2>&1 | tee "$check_log" || status=$?
+fi
+
+if [ "$status" -ne 0 ] && grep -q "^bwrap:" "$check_log"; then
+    bwrap_error="$(grep -m1 "^bwrap:" "$check_log")"
+    rm -f "$check_log"
+    failure_message="\`lake check\` could not start its sandbox (${bwrap_error}). Nothing was checked; this is a setup problem, not a finding about the project."
+    exit 2
+fi
+rm -f "$check_log"
+
+case "$status" in
+    0)
+        echo "lake check accepted the project"
+        ;;
+    1)
+        failure_message="\`lake check\` rejected the project: a checker rejected it, it uses an axiom that is not permitted, or the build did not succeed."
+        exit 1
+        ;;
+    2)
+        failure_message="\`lake check\` could not start: the project has no \`lake-manifest.json\`, or it has no default build targets. This is a setup problem, not a finding about the project."
+        exit 2
+        ;;
+    *)
+        failure_message="\`lake check\` exited with unexpected status ${status}."
+        exit "$status"
+        ;;
+esac