diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..4728532
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,369 @@
+name: "Lean CI (Parallel)"
+
+on:
+  workflow_call:
+    inputs:
+      auto-config:
+        description: |
+          Automatically configure based on Lake workspace.
+          Allowed values: "true" or "false".
+        type: string
+        required: false
+        default: "true"
+      build:
+        description: |
+          Run `lake build`.
+          Allowed values: "true" | "false" | "default".
+        type: string
+        required: false
+        default: "default"
+      test:
+        description: |
+          Run `lake test`.
+          Allowed values: "true" | "false" | "default".
+        type: string
+        required: false
+        default: "default"
+      lint:
+        description: |
+          Run `lake lint`.
+          Allowed values: "true" | "false" | "default".
+        type: string
+        required: false
+        default: "default"
+      mk_all-check:
+        description: |
+          Check all files are imported with `lake exe mk_all --check`.
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "false"
+      build-args:
+        description: |
+          Build arguments to pass to `lake build {build-args}`.
+        type: string
+        required: false
+        default: ""
+      test-args:
+        description: |
+          Test arguments to pass to `lake test {test-args}`.
+        type: string
+        required: false
+        default: ""
+      use-mathlib-cache:
+        description: |
+          Override automatic Mathlib detection.
+          Allowed values: "true" | "false" | "auto".
+        type: string
+        required: false
+        default: "auto"
+      use-github-cache:
+        description: |
+          Enable GitHub caching.
+          Allowed values: "true" or "false".
+        type: string
+        required: false
+        default: "true"
+      lake-package-directory:
+        description: |
+          Directory containing the Lake package.
+        type: string
+        required: false
+        default: "."
+      reinstall-transient-toolchain:
+        description: |
+          Uninstall lean-pr-release toolchains before running.
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "false"
+      check-reservoir-eligibility:
+        description: |
+          Check if repository is eligible for Reservoir.
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "false"
+      leanchecker:
+        description: |
+          Check environment with leanchecker.
+          Uses the bundled `leanchecker` binary on Lean `nightly-2026-01-09` / `v4.28.0-rc1` and newer.
+          Falls back to building the external `lean4checker` repository on older Lean versions.
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "false"
+      nanoda:
+        description: |
+          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).
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "false"
+      nanoda-allow-sorry:
+        description: |
+          When running nanoda, permit the sorryAx axiom.
+          Set to "false" if your project should have no sorry placeholders.
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "true"
+    outputs:
+      build-status:
+        description: "Status of lake build: SUCCESS | FAILURE | ''"
+        value: ${{ jobs.build.outputs.build-status }}
+      test-status:
+        description: "Status of lake test: SUCCESS | FAILURE | ''"
+        value: ${{ jobs.test.outputs.test-status }}
+      lint-status:
+        description: "Status of lake lint: SUCCESS | FAILURE | ''"
+        value: ${{ jobs.lint.outputs.lint-status }}
+      mk_all-status:
+        description: "Status of mk_all --check: SUCCESS | FAILURE | ''"
+        value: ${{ jobs.build.outputs.mk_all-status }}
+      detected-mathlib:
+        description: "Whether Mathlib dependency was detected"
+        value: ${{ jobs.build.outputs.detected-mathlib }}
+      nanoda-status:
+        description: "Status of nanoda check: SUCCESS | FAILURE | ''"
+        value: ${{ jobs.nanoda.outputs.nanoda-status }}
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    outputs:
+      run-lake-test: ${{ steps.config.outputs.run-lake-test }}
+      run-lake-lint: ${{ steps.config.outputs.run-lake-lint }}
+      build-status: ${{ steps.build.outputs.build-status }}
+      mk_all-status: ${{ steps.mk_all.outputs.mk_all-status }}
+      detected-mathlib: ${{ steps.detect-mathlib.outputs.detected-mathlib }}
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: install elan
+        run: |
+          : Install Elan
+          "${GITHUB_WORKSPACE}/scripts/install_elan.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - name: configure
+        id: config
+        env:
+          AUTO_CONFIG: ${{ inputs.auto-config }}
+          BUILD: ${{ inputs.build }}
+          TEST: ${{ inputs.test }}
+          LINT: ${{ inputs.lint }}
+        run: |
+          : Configure Lean Action
+          "${GITHUB_WORKSPACE}/scripts/config.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - name: reinstall transient toolchain
+        if: inputs.reinstall-transient-toolchain == 'true'
+        run: |
+          : Reinstall Transient Toolchains
+          if [[ "$(cat lean-toolchain)" =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
+            elan toolchain uninstall "$(cat lean-toolchain)"
+          fi
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - name: ensure all files are imported
+        id: mk_all
+        if: inputs.mk_all-check == 'true'
+        run: |
+          : Ensure all files are imported
+          "${GITHUB_WORKSPACE}/scripts/mk_all_check.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - uses: actions/cache/restore@v4
+        if: inputs.use-github-cache == 'true'
+        with:
+          path: ${{ inputs.lake-package-directory }}/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}
+
+      - name: detect mathlib
+        if: inputs.use-mathlib-cache == 'auto'
+        id: detect-mathlib
+        run: |
+          : Detect Mathlib
+          "${GITHUB_WORKSPACE}/scripts/detect_mathlib.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - name: get mathlib cache
+        if: steps.detect-mathlib.outputs.detected-mathlib == 'true' || inputs.use-mathlib-cache == 'true'
+        run: |
+          : Get Mathlib Cache
+          echo "::group::Mathlib Cache"
+          lake exe cache get
+          echo "::endgroup::"
+          echo
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - name: build
+        id: build
+        if: steps.config.outputs.run-lake-build == 'true'
+        env:
+          BUILD_ARGS: ${{ inputs.build-args }}
+        run: |
+          : Lake Build
+          "${GITHUB_WORKSPACE}/scripts/lake_build.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - uses: actions/cache/save@v4
+        if: inputs.use-github-cache == 'true'
+        with:
+          path: ${{ inputs.lake-package-directory }}/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+
+  test:
+    needs: build
+    if: needs.build.outputs.run-lake-test == 'true'
+    runs-on: ubuntu-latest
+    outputs:
+      test-status: ${{ steps.test.outputs.test-status }}
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: install elan
+        run: |
+          : Install Elan
+          "${GITHUB_WORKSPACE}/scripts/install_elan.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - uses: actions/cache/restore@v4
+        if: inputs.use-github-cache == 'true'
+        with:
+          path: ${{ inputs.lake-package-directory }}/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}
+
+      - name: test
+        id: test
+        env:
+          TEST_ARGS: ${{ inputs.test-args }}
+        run: |
+          : Lake Test
+          "${GITHUB_WORKSPACE}/scripts/lake_test.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+  lint:
+    needs: build
+    if: needs.build.outputs.run-lake-lint == 'true'
+    runs-on: ubuntu-latest
+    outputs:
+      lint-status: ${{ steps.lint.outputs.lint-status }}
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: install elan
+        run: |
+          : Install Elan
+          "${GITHUB_WORKSPACE}/scripts/install_elan.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - uses: actions/cache/restore@v4
+        if: inputs.use-github-cache == 'true'
+        with:
+          path: ${{ inputs.lake-package-directory }}/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}
+
+      - name: lint
+        id: lint
+        run: |
+          : Lake Lint
+          "${GITHUB_WORKSPACE}/scripts/lake_lint.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+  leanchecker:
+    needs: build
+    if: inputs.leanchecker == 'true'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: install elan
+        run: |
+          : Install Elan
+          "${GITHUB_WORKSPACE}/scripts/install_elan.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - uses: actions/cache/restore@v4
+        if: inputs.use-github-cache == 'true'
+        with:
+          path: ${{ inputs.lake-package-directory }}/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}
+
+      - name: leanchecker
+        run: |
+          : Check Environment with leanchecker
+          "${GITHUB_WORKSPACE}/scripts/run_leanchecker.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+  reservoir:
+    needs: build
+    if: inputs.check-reservoir-eligibility == 'true'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: check reservoir eligibility
+        run: |
+          : Check Reservoir Eligibility
+          "${GITHUB_WORKSPACE}/scripts/check_reservoir_eligibility.sh" \
+            "${{ github.event.repository.private }}" \
+            "${{ github.event.repository.stargazers_count }}" \
+            "${{ github.event.repository.license.spdx_id }}"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+  nanoda:
+    needs: build
+    if: inputs.nanoda == 'true'
+    runs-on: ubuntu-latest
+    outputs:
+      nanoda-status: ${{ steps.nanoda.outputs.nanoda-status }}
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: install elan
+        run: |
+          : Install Elan
+          "${GITHUB_WORKSPACE}/scripts/install_elan.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - uses: actions/cache/restore@v4
+        if: inputs.use-github-cache == 'true'
+        with:
+          path: ${{ inputs.lake-package-directory }}/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}
+
+      - name: nanoda
+        id: nanoda
+        env:
+          NANODA_ALLOW_SORRY: ${{ inputs.nanoda-allow-sorry }}
+        run: |
+          : Check Environment with nanoda
+          "${GITHUB_WORKSPACE}/scripts/run_nanoda.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
diff --git a/.github/workflows/nanoda-daily.yml b/.github/workflows/nanoda-daily.yml
new file mode 100644
index 0000000..f4a9b73
--- /dev/null
+++ b/.github/workflows/nanoda-daily.yml
@@ -0,0 +1,147 @@
+# Reusable workflow for daily nanoda verification
+# Users can call this workflow from their repository:
+#
+#   name: Daily nanoda verification
+#   on:
+#     schedule:
+#       - cron: '0 0 * * *'
+#     workflow_dispatch:
+#   jobs:
+#     verify:
+#       uses: leanprover/lean-action/.github/workflows/nanoda-daily.yml@v1
+#       secrets:
+#         webhook-url: ${{ secrets.WEBHOOK_URL }}      # optional
+#         zulip-api-key: ${{ secrets.ZULIP_API_KEY }}  # optional
+
+name: nanoda Daily Verification
+
+on:
+  workflow_call:
+    inputs:
+      allow-sorry:
+        description: 'Permit sorryAx axiom'
+        type: boolean
+        default: true
+      notify:
+        description: 'Notification method: issue, webhook, zulip, none'
+        type: string
+        default: 'issue'
+      zulip-stream:
+        description: 'Zulip stream name (if using zulip notify)'
+        type: string
+        default: 'ci'
+      zulip-topic:
+        description: 'Zulip topic (if using zulip notify)'
+        type: string
+        default: 'nanoda'
+      zulip-org-url:
+        description: 'Zulip organization URL (required if using zulip notify)'
+        type: string
+        default: ''
+    secrets:
+      webhook-url:
+        description: 'Slack/Discord webhook URL (optional)'
+        required: false
+      zulip-api-key:
+        description: 'Zulip bot API key (optional)'
+        required: false
+
+jobs:
+  nanoda-verify:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Run lean-action with nanoda
+        id: lean-action
+        uses: leanprover/lean-action@v1
+        with:
+          nanoda: true
+          nanoda-allow-sorry: ${{ inputs.allow-sorry }}
+
+      - name: Create GitHub issue on failure
+        if: failure() && inputs.notify == 'issue'
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const runUrl = `${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`;
+            await github.rest.issues.create({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              title: '❌ Daily nanoda verification failed',
+              body: `The daily nanoda type checker verification failed.\n\n**Commit:** ${context.sha}\n**Run:** [View workflow run](${runUrl})\n\nPlease investigate and fix any type checking issues.`,
+              labels: ['nanoda', 'automated', 'ci-failure']
+            });
+
+      - name: Send webhook notification
+        if: always() && inputs.notify == 'webhook'
+        env:
+          WEBHOOK_URL: ${{ secrets.webhook-url }}
+        run: |
+          if [ -z "$WEBHOOK_URL" ]; then
+            echo "::error::webhook-url secret is required when notify is set to 'webhook'"
+            exit 1
+          fi
+          STATUS="${{ job.status }}"
+          EMOJI=$([[ "$STATUS" == "success" ]] && echo "✅" || echo "❌")
+          RUN_URL="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
+
+          curl --fail -X POST "$WEBHOOK_URL" \
+            -H "Content-Type: application/json" \
+            -d "{
+              \"text\": \"$EMOJI nanoda daily verification: $STATUS\",
+              \"blocks\": [
+                {
+                  \"type\": \"section\",
+                  \"text\": {
+                    \"type\": \"mrkdwn\",
+                    \"text\": \"$EMOJI *nanoda daily verification*: $STATUS\n<$RUN_URL|View run> | Commit: \`${{ github.sha }}\`\"
+                  }
+                }
+              ]
+            }"
+        shell: bash
+
+      - name: Validate Zulip configuration
+        id: validate-zulip
+        if: (success() || failure()) && inputs.notify == 'zulip'
+        continue-on-error: true
+        env:
+          ZULIP_ORG_URL: ${{ inputs.zulip-org-url }}
+          ZULIP_API_KEY: ${{ secrets.zulip-api-key }}
+        run: |
+          if [ -z "$ZULIP_ORG_URL" ]; then
+            echo "::error::zulip-org-url input is required when notify is set to 'zulip'"
+            exit 1
+          fi
+          if [ -z "$ZULIP_API_KEY" ]; then
+            echo "::error::zulip-api-key secret is required when notify is set to 'zulip'"
+            exit 1
+          fi
+
+      - name: Send Zulip notification on success
+        if: success() && inputs.notify == 'zulip' && steps.validate-zulip.outcome == 'success'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5
+        with:
+          api-key: ${{ secrets.zulip-api-key }}
+          email: 'github-bot@${{ inputs.zulip-org-url }}'
+          organization-url: 'https://${{ inputs.zulip-org-url }}'
+          to: ${{ inputs.zulip-stream }}
+          type: 'stream'
+          topic: ${{ inputs.zulip-topic }}
+          content: |
+            ✅ nanoda daily verification [succeeded](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) on `${{ github.sha }}`
+
+      - name: Send Zulip notification on failure
+        if: steps.lean-action.outcome == 'failure' && inputs.notify == 'zulip' && steps.validate-zulip.outcome == 'success'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5
+        with:
+          api-key: ${{ secrets.zulip-api-key }}
+          email: 'github-bot@${{ inputs.zulip-org-url }}'
+          organization-url: 'https://${{ inputs.zulip-org-url }}'
+          to: ${{ inputs.zulip-stream }}
+          type: 'stream'
+          topic: '${{ inputs.zulip-topic }} failure'
+          content: |
+            ❌ nanoda daily verification [failed](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) on `${{ github.sha }}`
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a2f1fe7..5914913 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Added
+
+- new parallel reusable workflow `.github/workflows/ci.yml` that runs test, lint, leanchecker, nanoda, and reservoir checks in parallel
+- new `nanoda` input to check environment with [nanoda](https://github.com/ammkrn/nanoda_lib) external type checker
+- new `nanoda-allow-sorry` input to permit sorryAx axiom when running nanoda (default: true)
+- new `nanoda-status` output parameter
+- new reusable workflow `nanoda-daily.yml` for scheduled daily verification with notifications
+
 ### Changed
 
 - rename the `lean4checker` input to `leanchecker`, while keeping `lean4checker` as a deprecated alias
diff --git a/README.md b/README.md
index 77eb4fe..0c9f3cd 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`
+- `nanoda`
 
 ### Automatic configuration
 
@@ -137,6 +138,36 @@ because `lean-action` may not detect the `test_driver` in the Lake workspace.
 
 To be certain `lean-action` runs a step, specify the desire feature with a feature input.
 
+## Parallel Workflow
+
+For faster CI, `lean-action` provides a reusable workflow that runs test, lint, leanchecker, nanoda, and reservoir checks in parallel on separate runners:
+
+```yaml
+name: CI
+
+on:
+  push:
+    branches: ["main"]
+  pull_request:
+    branches: ["main"]
+
+jobs:
+  ci:
+    uses: leanprover/lean-action/.github/workflows/ci.yml@v1
+    with:
+      test: "true"
+      lint: "true"
+      leanchecker: "true"
+      nanoda: "true"
+```
+
+The parallel workflow:
+- Runs a **build** job first (elan setup, config, mathlib cache, lake build)
+- Then runs **test**, **lint**, **leanchecker**, **nanoda**, and **reservoir** jobs in parallel
+- Each parallel job restores the build cache from the build job
+
+All inputs from the standard action are supported. The workflow outputs the same status parameters (`build-status`, `test-status`, `lint-status`, `mk_all-status`, `nanoda-status`).
+
 ## Customization
 
 `lean-action` provides optional configuration inputs to customize the behavior for your specific workflow.
@@ -204,7 +235,20 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
 
     # Deprecated alias for `leanchecker`.
     lean4checker: ""
-    
+
+    # 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).
+    # Allowed values: "true" | "false".
+    # Default: "false"
+    nanoda: ""
+
+    # When running nanoda, permit the sorryAx axiom.
+    # Set to "false" if your project should have no sorry placeholders.
+    # Allowed values: "true" | "false".
+    # Default: "true"
+    nanoda-allow-sorry: ""
+
     # Enable GitHub caching.
     # Allowed values: "true" or "false".
     # If use-github-cache input is not provided, the action will use GitHub caching by default.
@@ -238,6 +282,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" | ""
+- `nanoda-status`
+  - Values: "SUCCESS" | "FAILURE" | ""
 
 Note, a value of empty string indicates `lean-action` did not run the corresponding feature.
 
@@ -302,6 +348,60 @@ steps:
       rm import_graph.dot
 ```
 
+## External Type Checking with nanoda
+
+[nanoda](https://github.com/ammkrn/nanoda_lib) is an independent Lean 4 type checker written in Rust. It provides additional assurance that your project's declarations are well-typed by verifying them with a completely separate implementation.
+
+### Enable nanoda verification
+
+```yaml
+- uses: leanprover/lean-action@v1
+  with:
+    nanoda: true
+```
+
+### Require no sorry placeholders
+
+By default, nanoda permits the `sorryAx` axiom for projects with incomplete proofs. To require all proofs be complete:
+
+```yaml
+- uses: leanprover/lean-action@v1
+  with:
+    nanoda: true
+    nanoda-allow-sorry: false
+```
+
+### Daily nanoda verification with notifications
+
+For daily verification runs with automatic failure notifications, use the reusable workflow:
+
+```yaml
+# .github/workflows/nanoda-daily.yml
+name: Daily nanoda verification
+on:
+  schedule:
+    - cron: '0 0 * * *'
+  workflow_dispatch:
+
+jobs:
+  verify:
+    uses: leanprover/lean-action/.github/workflows/nanoda-daily.yml@v1
+    # Optional: configure notification method
+    # with:
+    #   notify: 'issue'  # default: creates GitHub issue on failure
+    # For webhook (Slack/Discord):
+    # with:
+    #   notify: 'webhook'
+    # secrets:
+    #   webhook-url: ${{ secrets.WEBHOOK_URL }}
+    # For Zulip:
+    # with:
+    #   notify: 'zulip'
+    #   zulip-org-url: 'leanprover.zulipchat.com'
+    # secrets:
+    #   zulip-api-key: ${{ secrets.ZULIP_API_KEY }}
+```
+
 ## Projects which use `lean-action`
 
 - [leanprover-community/aesop](https://github.com/leanprover-community/aesop/blob/master/.github/workflows/build.yml#L16)
diff --git a/action.yml b/action.yml
index 494ffc4..c54c250 100644
--- a/action.yml
+++ b/action.yml
@@ -91,6 +91,21 @@ inputs:
       Allowed values: "true" | "false".
     required: false
     default: "false"
+  nanoda:
+    description: |
+      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).
+      Allowed values: "true" | "false".
+    required: false
+    default: "false"
+  nanoda-allow-sorry:
+    description: |
+      When running nanoda, permit the sorryAx axiom.
+      Set to "false" if your project should have no sorry placeholders.
+      Allowed values: "true" | "false".
+    required: false
+    default: "true"
   use-github-cache:
     description: |
       Enable GitHub caching.
@@ -138,6 +153,11 @@ outputs:
       If lean-action detected a mathlib dependency equals "true"
       otherwise equals "false".
     value: ${{ steps.detect-mathlib.outputs.detected-mathlib }}
+  nanoda-status:
+    description: |
+      The status of the nanoda check step.
+      Allowed values: "SUCCESS" | "FAILURE" | "".
+    value: ${{ steps.nanoda.outputs.nanoda-status }}
 
 runs:
   using: "composite"
@@ -271,3 +291,14 @@ runs:
         ${GITHUB_ACTION_PATH}/scripts/run_leanchecker.sh
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
+
+    - name: check environment with nanoda
+      id: nanoda
+      if: ${{ inputs.nanoda == 'true' }}
+      env:
+        NANODA_ALLOW_SORRY: ${{ inputs.nanoda-allow-sorry }}
+      run: |
+        : Check Environment with nanoda
+        ${GITHUB_ACTION_PATH}/scripts/run_nanoda.sh
+      shell: bash
+      working-directory: ${{ inputs.lake-package-directory }}
diff --git a/scripts/run_nanoda.sh b/scripts/run_nanoda.sh
new file mode 100755
index 0000000..ca87f03
--- /dev/null
+++ b/scripts/run_nanoda.sh
@@ -0,0 +1,131 @@
+#!/bin/bash
+set -e
+
+# Group logging using the ::group:: workflow command
+echo "::group::nanoda Output"
+echo "Checking environment with nanoda external type checker"
+
+# handle_exit function to capture exit status and cleanup
+handle_exit() {
+    exit_status=$?
+
+    # Close the log group before cleanup
+    echo "::endgroup::"
+
+    # Always cleanup temporary files/directories
+    echo "Cleaning up temporary files..."
+    rm -rf _lean4export _nanoda_lib _nanoda_export.txt _nanoda_config.json
+
+    if [ $exit_status -ne 0 ]; then
+        echo "nanoda-status=FAILURE" >> "$GITHUB_OUTPUT"
+        echo "::error::nanoda check failed"
+    else
+        echo "nanoda-status=SUCCESS" >> "$GITHUB_OUTPUT"
+        echo
+    fi
+}
+trap handle_exit EXIT
+
+# Check for conflicting directories before we start
+if [ -d "_lean4export" ] || [ -d "_nanoda_lib" ]; then
+    echo "::error::Directories _lean4export or _nanoda_lib already exist. Please remove them before running nanoda."
+    exit 1
+fi
+
+# Step 1: Install Rust if not present
+echo "Checking for Rust installation..."
+if ! command -v cargo &> /dev/null; then
+    echo "Installing Rust toolchain..."
+    curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile minimal
+    # shellcheck source=/dev/null
+    source "$HOME/.cargo/env"
+else
+    echo "Rust already installed: $(cargo --version)"
+fi
+
+# Step 2: Clone and build lean4export
+echo "Cloning and building lean4export..."
+git clone --depth 1 https://github.com/leanprover/lean4export.git _lean4export
+
+# Copy lean-toolchain to lean4export so it uses matching Lean version
+cp lean-toolchain _lean4export/
+
+(
+    cd _lean4export
+    lake build
+)
+
+# Step 3: Clone and build nanoda_lib
+echo "Cloning and building nanoda_lib..."
+# Using debug branch which has fixes for recent Lean kernel changes
+git clone --depth 1 --branch debug https://github.com/ammkrn/nanoda_lib.git _nanoda_lib
+
+(
+    cd _nanoda_lib
+    cargo build --release
+)
+
+# Step 4: Detect module name from lakefile
+echo "Detecting module name..."
+MODULE_NAME=""
+
+# Try lakefile.toml first
+if [ -f "lakefile.toml" ]; then
+    # Extract name from [package] section
+    MODULE_NAME=$(grep -A5 '^\[package\]' lakefile.toml | grep '^name' | head -1 | sed 's/.*= *"\([^"]*\)".*/\1/' || true)
+fi
+
+# Fallback to lakefile.lean
+if [ -z "$MODULE_NAME" ] && [ -f "lakefile.lean" ]; then
+    # Try to extract from 'package' declaration (allowing leading whitespace)
+    MODULE_NAME=$(grep -E "^\s*package\s+" lakefile.lean | head -1 | awk '{print $2}' || true)
+fi
+
+if [ -z "$MODULE_NAME" ]; then
+    echo "::error::Could not detect module name from lakefile.toml or lakefile.lean"
+    exit 1
+fi
+
+echo "Detected module name: $MODULE_NAME"
+
+# Step 5: Export the project
+echo "Exporting $MODULE_NAME..."
+EXPORT_FILE="_nanoda_export.txt"
+lake env _lean4export/.lake/build/bin/lean4export "$MODULE_NAME" > "$EXPORT_FILE"
+
+echo "Export file size: $(wc -c < "$EXPORT_FILE") bytes"
+echo "Export file lines: $(wc -l < "$EXPORT_FILE") lines"
+
+# Step 6: Create nanoda config
+echo "Creating nanoda configuration..."
+CONFIG_FILE="_nanoda_config.json"
+
+# Build permitted_axioms array
+PERMITTED_AXIOMS='["propext", "Classical.choice", "Quot.sound", "Lean.trustCompiler"'
+if [ "$NANODA_ALLOW_SORRY" = "true" ]; then
+    PERMITTED_AXIOMS="$PERMITTED_AXIOMS, \"sorryAx\""
+    echo "Note: sorryAx axiom is permitted"
+fi
+PERMITTED_AXIOMS="$PERMITTED_AXIOMS]"
+
+cat > "$CONFIG_FILE" << EOF
+{
+    "export_file_path": "$EXPORT_FILE",
+    "use_stdin": false,
+    "permitted_axioms": $PERMITTED_AXIOMS,
+    "unpermitted_axiom_hard_error": false,
+    "nat_extension": true,
+    "string_extension": true,
+    "print_success_message": true
+}
+EOF
+
+echo "Config file contents:"
+cat "$CONFIG_FILE"
+
+# Step 7: Run nanoda
+echo ""
+echo "Running nanoda type checker..."
+_nanoda_lib/target/release/nanoda_bin "$CONFIG_FILE"
+
+echo "nanoda check completed successfully"