diff --git a/CHANGELOG.md b/CHANGELOG.md
index a2e195b..d322bf6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Added
+
+- new `leanchecker-args` input to pass arguments to `lake env leanchecker`,
+  e.g. `leanchecker-args: "-v"` for verbose output or explicit module prefixes
+  such as `leanchecker-args: "MyPkg.Core"` to narrow the set of modules checked
+
 ## v1.5.0 - 2026-04-21
 
 ### Added
diff --git a/README.md b/README.md
index 07b4b66..4839cab 100644
--- a/README.md
+++ b/README.md
@@ -203,6 +203,13 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Default: "false"
     leanchecker: ""
 
+    # Extra arguments to pass to `lake env leanchecker {leanchecker-args}`.
+    # For example, `leanchecker-args: "-v"` enables verbose output, and
+    # `leanchecker-args: "MyPkg.Core MyPkg.Extras"` restricts checking to the
+    # listed module prefixes. Only takes effect when `leanchecker: true`.
+    # Default: ""
+    leanchecker-args: ""
+
     # Deprecated alias for `leanchecker`.
     lean4checker: ""
 
diff --git a/action.yml b/action.yml
index c54c250..143fbfe 100644
--- a/action.yml
+++ b/action.yml
@@ -83,6 +83,16 @@ inputs:
       Allowed values: "true" | "false".
     required: false
     default: "false"
+  leanchecker-args:
+    description: |
+      Extra arguments to pass to `lake env leanchecker {leanchecker-args}`.
+      For example, `leanchecker-args: "-v"` enables verbose output, and
+      `leanchecker-args: "MyPkg.Core MyPkg.Extras"` restricts checking to the
+      listed module prefixes.
+      By default, `lean-action` calls `lake env leanchecker` with no arguments,
+      which checks every module in the root package.
+    required: false
+    default: ""
   lean4checker:
     description: |
       Deprecated alias for `leanchecker`.
@@ -286,6 +296,7 @@ runs:
       env:
         LEANCHECKER_INPUT: ${{ inputs.leanchecker }}
         LEAN4CHECKER_INPUT: ${{ inputs.lean4checker }}
+        LEANCHECKER_ARGS: ${{ inputs.leanchecker-args }}
       run: |
         : Check Environment with leanchecker
         ${GITHUB_ACTION_PATH}/scripts/run_leanchecker.sh
diff --git a/scripts/run_leanchecker.sh b/scripts/run_leanchecker.sh
index 04006f6..61e2bfd 100755
--- a/scripts/run_leanchecker.sh
+++ b/scripts/run_leanchecker.sh
@@ -11,7 +11,8 @@ fi
 leanchecker_path="$(elan which leanchecker 2>/dev/null || true)"
 if [ -n "$leanchecker_path" ] && [ -x "$leanchecker_path" ]; then
   echo "Using bundled leanchecker from the active Lean toolchain"
-  lake env leanchecker
+  # use eval to ensure leanchecker arguments are expanded
+  eval "lake env leanchecker ${LEANCHECKER_ARGS:-}"
   echo "::endgroup::"
   echo
   exit 0
@@ -40,7 +41,8 @@ fi
 )
 
 echo "Running external lean4checker"
-lake env lean4checker/.lake/build/bin/lean4checker
+# use eval to ensure leanchecker arguments are expanded
+eval "lake env lean4checker/.lake/build/bin/lean4checker ${LEANCHECKER_ARGS:-}"
 
 echo "::endgroup::"
 echo