diff --git a/CLAUDE.md b/CLAUDE.md
index 00a0d4de7..29ae2e450 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -32,7 +32,7 @@ make test-unit
 make test-integration
 
 # Run a single test
-uv --directory kmir run pytest kmir/src/tests/integration/test_prove.py::test_prove_rs -k "test_name"
+uv --directory kmir run pytest kmir/src/tests/integration/test_prove.py::test_prove -k "test_name"
 
 # Generate and parse SMIR for test files
 make smir-parse-tests
@@ -61,7 +61,7 @@ source kmir/.venv/bin/activate
 uv --directory kmir run kmir <command>
 
 # Prove Rust code directly (recommended)
-uv --directory kmir run kmir prove-rs path/to/file.rs --verbose
+uv --directory kmir run kmir prove path/to/file.rs --verbose
 
 # Generate SMIR JSON from Rust
 ./scripts/generate-smir-json.sh file.rs output_dir
@@ -79,7 +79,7 @@ uv --directory kmir run kmir show proof_id --proof-dir ./proof_dir
     - `smir.py` - SMIR JSON parsing and info extraction
     - `kdist/mir-semantics/` - K semantics definitions
   - `src/tests/` - Test suites
-    - `integration/data/prove-rs/` - Rust test programs for prove-rs
+    - `integration/data/prove-rs/` - Rust test programs for prove
     - `integration/data/exec-smir/` - Rust programs for execution tests
 
 ### Key K Semantics Files
@@ -105,17 +105,17 @@ Intrinsic functions (like `black_box`, `raw_eq`) don't have regular function bod
 
 ## Testing Patterns
 
-### prove-rs Tests
+### prove Tests
 Tests in `kmir/src/tests/integration/data/prove-rs/` follow this pattern:
 - Simple Rust programs with assertions
 - File naming: `test-name.rs` (passes), `test-name-fail.rs` (expected to fail)
-- Tests run via `kmir prove-rs` command
+- Tests run via `kmir prove` command
 - Generate SMIR automatically during test execution
 
 ### Adding New Tests
 1. Add Rust file to `prove-rs/` directory
 2. Use assertions to verify behavior
-3. Run with: `uv --directory kmir run kmir prove-rs your-test.rs`
+3. Run with: `uv --directory kmir run kmir prove your-test.rs`
 
 ## Development Workflow
 
diff --git a/README.md b/README.md
index 40cf7736c..2d8b17566 100644
--- a/README.md
+++ b/README.md
@@ -70,7 +70,7 @@ Every subcommand supports `--help` for the full option list.
 | Command | Purpose |
 | --- | --- |
 | `kmir run` | Execute a Rust program from SMIR JSON |
-| `kmir prove-rs` | Prove properties of a Rust source file (recommended entry point) |
+| `kmir prove` | Prove properties of a Rust source file (recommended entry point) |
 | `kmir show` | Inspect a proof graph — nodes, deltas, rules, statistics |
 | `kmir view` | Interactive proof viewer |
 | `kmir prune` | Remove a node (and its subtree) from a proof |
@@ -82,7 +82,7 @@ Every subcommand supports `--help` for the full option list.
 
 ```bash
 # 1. Run a proof
-uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --verbose
+uv --project kmir run kmir prove program.rs --proof-dir ./proofs --verbose
 
 # 2. Overview — see all leaves and statistics
 uv --project kmir run kmir show proof_id --proof-dir ./proofs --leaves --statistics
@@ -104,11 +104,11 @@ When a proof does not close, the typical cycle is **inspect → refine → re-pr
 
 ```bash
 # Narrow down where things go wrong — break on every function call
-uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \
+uv --project kmir run kmir prove program.rs --proof-dir ./proofs \
     --break-on-calls --max-depth 200
 
 # Or break only when a specific function is entered
-uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \
+uv --project kmir run kmir prove program.rs --proof-dir ./proofs \
     --break-on-function "my_module::suspect_fn"
 
 # Split a large edge to find the exact divergence point
@@ -116,15 +116,15 @@ uv --project kmir run kmir section-edge proof_id "4,5" --proof-dir ./proofs --se
 
 # Prune a bad subtree and re-run
 uv --project kmir run kmir prune proof_id 5 --proof-dir ./proofs
-uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs
+uv --project kmir run kmir prove program.rs --proof-dir ./proofs
 
 # Export a proof subgraph as a reusable K module
 uv --project kmir run kmir show proof_id --proof-dir ./proofs --to-module lemma.json --minimize-proof
 # then re-prove with the lemma
-uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --add-module lemma.json
+uv --project kmir run kmir prove program.rs --proof-dir ./proofs --add-module lemma.json
 ```
 
-Other useful `prove-rs` break flags: `--break-every-step`, `--break-every-terminator`, `--break-on-thunk`, `--terminate-on-thunk`.
+Other useful `prove` break flags: `--break-every-step`, `--break-every-terminator`, `--break-on-thunk`, `--terminate-on-thunk`.
 
 ### Generate Stable MIR JSON manually
 
diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
index 42d71ce5d..b2ace6887 100644
--- a/kmir/src/kmir/__main__.py
+++ b/kmir/src/kmir/__main__.py
@@ -21,7 +21,7 @@
 from .options import (
     InfoOpts,
     LinkOpts,
-    ProveRSOpts,
+    ProveOpts,
     PruneOpts,
     RunOpts,
     SectionEdgeOpts,
@@ -72,8 +72,8 @@ def run(target_dir: Path):
             run(target_dir=Path(target_dir))
 
 
-def _kmir_prove_rs(opts: ProveRSOpts) -> None:
-    proof = KMIR.prove_rs(opts)
+def _kmir_prove(opts: ProveOpts) -> None:
+    proof = KMIR.prove_program(opts)
     print(str(proof.summary))
     if not proof.passed:
         sys.exit(1)
@@ -268,8 +268,8 @@ def kmir(args: Sequence[str]) -> None:
             _kmir_prune(opts)
         case SectionEdgeOpts():
             _kmir_section_edge(opts)
-        case ProveRSOpts():
-            _kmir_prove_rs(opts)
+        case ProveOpts():
+            _kmir_prove(opts)
         case LinkOpts():
             _kmir_link(opts)
         case _:
@@ -542,26 +542,24 @@ def _arg_parser() -> ArgumentParser:
     section_edge_parser.add_argument('--haskell-target', metavar='TARGET', help='Haskell target to use')
     section_edge_parser.add_argument('--llvm-lib-target', metavar='TARGET', help='LLVM lib target to use')
 
-    prove_rs_parser = command_parser.add_parser(
-        'prove-rs', help='Prove a rust program', parents=[kcli_args.logging_args, prove_args]
+    prove_parser = command_parser.add_parser(
+        'prove', help='Prove a Rust program', aliases=['prove-rs'], parents=[kcli_args.logging_args, prove_args]
     )
-    prove_rs_parser.add_argument(
-        'rs_file', type=Path, metavar='FILE', help='Rust file with the spec function (e.g. main)'
-    )
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument('rs_file', type=Path, metavar='FILE', help='Rust file with the spec function (e.g. main)')
+    prove_parser.add_argument(
         '--save-smir', action='store_true', help='Do not delete the intermediate generated SMIR JSON file.'
     )
-    prove_rs_parser.add_argument('--smir', action='store_true', help='Treat the input file as a smir json.')
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument('--smir', action='store_true', help='Treat the input file as a smir json.')
+    prove_parser.add_argument(
         '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
     )
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument(
         '--add-module',
         type=Path,
         metavar='FILE',
         help='K module file to include (.json format from --to-module)',
     )
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument(
         '--max-workers', metavar='N', type=int, help='Maximum number of workers for parallel exploration'
     )
 
@@ -640,8 +638,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 haskell_target=ns.haskell_target,
                 llvm_lib_target=ns.llvm_lib_target,
             )
-        case 'prove-rs':
-            return ProveRSOpts(
+        case 'prove' | 'prove-rs':
+            return ProveOpts(
                 rs_file=Path(ns.rs_file),
                 proof_dir=ns.proof_dir,
                 haskell_target=ns.haskell_target,
diff --git a/kmir/src/kmir/_prove.py b/kmir/src/kmir/_prove.py
index 45c6966b5..de729adf8 100644
--- a/kmir/src/kmir/_prove.py
+++ b/kmir/src/kmir/_prove.py
@@ -25,13 +25,13 @@
 
     from pyk.kast.inner import KInner
 
-    from .options import ProveRSOpts
+    from .options import ProveOpts
 
 
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-def prove_rs(opts: ProveRSOpts) -> APRProof:
+def prove(opts: ProveOpts) -> APRProof:
     if not opts.rs_file.is_file():
         raise ValueError(f'Input file does not exist: {opts.rs_file}')
 
@@ -42,14 +42,14 @@ def prove_rs(opts: ProveRSOpts) -> APRProof:
 
     if opts.proof_dir is not None:
         target_path = opts.proof_dir / label
-        return _prove_rs(opts, target_path, label)
+        return _prove(opts, target_path, label)
 
     with tempfile.TemporaryDirectory() as tmp_dir:
         target_path = Path(tmp_dir)
-        return _prove_rs(opts, target_path, label)
+        return _prove(opts, target_path, label)
 
 
-def _prove_rs(opts: ProveRSOpts, target_path: Path, label: str) -> APRProof:
+def _prove(opts: ProveOpts, target_path: Path, label: str) -> APRProof:
     if not opts.reload and opts.proof_dir is not None and APRProof.proof_data_exists(label, opts.proof_dir):
         _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {label}')
         proof = APRProof.read_proof_data(opts.proof_dir, label)
@@ -67,7 +67,9 @@ def _prove_rs(opts: ProveRSOpts, target_path: Path, label: str) -> APRProof:
         )
     else:
         _LOGGER.info(f'Constructing initial proof: {label}')
-        if opts.smir:
+        if opts.parsed_smir is not None:
+            smir_info = SMIRInfo(opts.parsed_smir)
+        elif opts.smir:
             smir_info = SMIRInfo.from_file(opts.rs_file)
         else:
             smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir))
@@ -138,7 +140,7 @@ def _prove_parallel(
     kmir: KMIR,
     proof: APRProof,
     *,
-    opts: ProveRSOpts,
+    opts: ProveOpts,
     label: str,
     cut_point_rules: list[str],
 ) -> None:
@@ -192,7 +194,7 @@ def _prove_sequential(
     kmir: KMIR,
     proof: APRProof,
     *,
-    opts: ProveRSOpts,
+    opts: ProveOpts,
     label: str,
     cut_point_rules: list[str],
 ) -> None:
diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py
index 396c5407a..d283d5ba0 100644
--- a/kmir/src/kmir/kmir.py
+++ b/kmir/src/kmir/kmir.py
@@ -33,7 +33,7 @@
     from pyk.proof.reachability import APRProof
     from pyk.utils import BugReport
 
-    from .options import DisplayOpts, ProveRSOpts
+    from .options import DisplayOpts, ProveOpts
 
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -121,10 +121,10 @@ def run_smir(
         return result
 
     @staticmethod
-    def prove_rs(opts: ProveRSOpts) -> APRProof:
-        from ._prove import prove_rs
+    def prove_program(opts: ProveOpts) -> APRProof:
+        from ._prove import prove
 
-        return prove_rs(opts)
+        return prove(opts)
 
 
 class KMIRSemantics(DefaultSemantics):
diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py
index addc13a1f..2a65d20dc 100644
--- a/kmir/src/kmir/options.py
+++ b/kmir/src/kmir/options.py
@@ -61,15 +61,22 @@ class ProofOpts(KMirOpts):
 
 @dataclass
 class ProveOpts(KMirOpts):
+    rs_file: Path
     proof_dir: Path | None
     haskell_target: str | None
     llvm_lib_target: str | None
     bug_report: Path | None
     max_depth: int | None
     max_iterations: int | None
+    max_workers: int | None
     reload: bool
     fail_fast: bool
     maintenance_rate: int
+    save_smir: bool
+    smir: bool
+    parsed_smir: dict | None
+    start_symbol: str
+    add_module: Path | None
     break_on_calls: bool
     break_on_function_calls: bool
     break_on_intrinsic_calls: bool
@@ -87,71 +94,6 @@ class ProveOpts(KMirOpts):
     terminate_on_thunk: bool
     break_on_function: list[str]
 
-    def __init__(
-        self,
-        *,
-        proof_dir: Path | str | None = None,
-        haskell_target: str | None = None,
-        llvm_lib_target: str | None = None,
-        bug_report: Path | None = None,
-        max_depth: int | None = None,
-        max_iterations: int | None = None,
-        reload: bool = False,
-        fail_fast: bool = False,
-        maintenance_rate: int = 1,
-        break_on_calls: bool = False,
-        break_on_function_calls: bool = False,
-        break_on_intrinsic_calls: bool = False,
-        break_on_thunk: bool = False,
-        break_every_statement: bool = False,
-        break_on_terminator_goto: bool = False,
-        break_on_terminator_switch_int: bool = False,
-        break_on_terminator_return: bool = False,
-        break_on_terminator_call: bool = False,
-        break_on_terminator_assert: bool = False,
-        break_on_terminator_drop: bool = False,
-        break_on_terminator_unreachable: bool = False,
-        break_every_terminator: bool = False,
-        break_every_step: bool = False,
-        terminate_on_thunk: bool = False,
-        break_on_function: list[str] | None = None,
-    ) -> None:
-        self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
-        self.haskell_target = haskell_target
-        self.llvm_lib_target = llvm_lib_target
-        self.bug_report = bug_report
-        self.max_depth = max_depth
-        self.max_iterations = max_iterations
-        self.reload = reload
-        self.fail_fast = fail_fast
-        self.maintenance_rate = maintenance_rate
-        self.break_on_calls = break_on_calls
-        self.break_on_function_calls = break_on_function_calls
-        self.break_on_intrinsic_calls = break_on_intrinsic_calls
-        self.break_on_thunk = break_on_thunk
-        self.break_every_statement = break_every_statement
-        self.break_on_terminator_goto = break_on_terminator_goto
-        self.break_on_terminator_switch_int = break_on_terminator_switch_int
-        self.break_on_terminator_return = break_on_terminator_return
-        self.break_on_terminator_call = break_on_terminator_call
-        self.break_on_terminator_assert = break_on_terminator_assert
-        self.break_on_terminator_drop = break_on_terminator_drop
-        self.break_on_terminator_unreachable = break_on_terminator_unreachable
-        self.break_every_terminator = break_every_terminator
-        self.break_every_step = break_every_step
-        self.terminate_on_thunk = terminate_on_thunk
-        self.break_on_function = break_on_function if break_on_function is not None else []
-
-
-@dataclass
-class ProveRSOpts(ProveOpts):
-    rs_file: Path
-    save_smir: bool
-    smir: bool
-    start_symbol: str
-    add_module: Path | None
-    max_workers: int | None
-
     def __init__(
         self,
         rs_file: Path,
@@ -168,6 +110,7 @@ def __init__(
         maintenance_rate: int = 1,
         save_smir: bool = False,
         smir: bool = False,
+        parsed_smir: dict | None = None,
         start_symbol: str = 'main',
         break_on_calls: bool = False,
         break_on_function_calls: bool = False,
@@ -200,6 +143,7 @@ def __init__(
         self.maintenance_rate = maintenance_rate
         self.save_smir = save_smir
         self.smir = smir
+        self.parsed_smir = parsed_smir
         self.start_symbol = start_symbol
         self.break_on_calls = break_on_calls
         self.break_on_function_calls = break_on_function_calls
diff --git a/kmir/src/tests/integration/test_cli.py b/kmir/src/tests/integration/test_cli.py
index 33812669b..78a440453 100644
--- a/kmir/src/tests/integration/test_cli.py
+++ b/kmir/src/tests/integration/test_cli.py
@@ -7,7 +7,7 @@
 import pytest
 
 from kmir.__main__ import _kmir_info, _kmir_link, _kmir_prune, _kmir_show
-from kmir.options import InfoOpts, LinkOpts, ProveRSOpts, PruneOpts, ShowOpts
+from kmir.options import InfoOpts, LinkOpts, ProveOpts, PruneOpts, ShowOpts
 from kmir.smir import SMIRInfo
 from kmir.testing.fixtures import assert_or_update_show_output
 
@@ -16,7 +16,7 @@
 
     from kmir.kmir import KMIR
 
-PROVE_RS_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
+PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
 # Repo root: used to normalise absolute paths in expected-output snapshots so
 # they don't differ between local checkouts and CI (e.g. symbolic-args-fail.main.cli-stats-leaves).
 _REPO_ROOT = str(Path(__file__).resolve().parents[4])
@@ -31,8 +31,8 @@ def _prove_and_store(
     is_smir: bool = False,
     max_depth: int | None = None,
 ) -> APRProof:
-    opts = ProveRSOpts(rs_or_json, proof_dir=tmp_path, smir=is_smir, start_symbol=start_symbol, max_depth=max_depth)
-    apr_proof = kmir.prove_rs(opts)
+    opts = ProveOpts(rs_or_json, proof_dir=tmp_path, smir=is_smir, start_symbol=start_symbol, max_depth=max_depth)
+    apr_proof = kmir.prove_program(opts)
     apr_proof.write_proof_data()
     return apr_proof
 
@@ -40,7 +40,7 @@ def _prove_and_store(
 def test_cli_show_printers_snapshot(
     kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str], update_expected_output: bool
 ) -> None:
-    rs_file = PROVE_RS_DIR / 'assert-true.rs'
+    rs_file = PROVE_DIR / 'assert-true.rs'
     start_symbol = 'main'
     apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False)
 
@@ -57,7 +57,7 @@ def test_cli_show_printers_snapshot(
     out_custom = capsys.readouterr().out.rstrip()
     assert_or_update_show_output(
         out_custom,
-        PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-custom-printer.expected',
+        PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-custom-printer.expected',
         update=update_expected_output,
     )
 
@@ -74,7 +74,7 @@ def test_cli_show_printers_snapshot(
     out_default = capsys.readouterr().out.rstrip()
     assert_or_update_show_output(
         out_default,
-        PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-default-printer.expected',
+        PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-default-printer.expected',
         update=update_expected_output,
     )
 
@@ -83,7 +83,7 @@ def test_cli_show_printers_snapshot(
     'src,start_symbol,is_smir',
     [
         pytest.param(
-            (PROVE_RS_DIR / 'symbolic-args-fail.rs'),
+            (PROVE_DIR / 'symbolic-args-fail.rs'),
             'main',
             False,
             id='symbolic-args-fail.main',
@@ -122,14 +122,14 @@ def test_cli_show_statistics_and_leaves(
 
     assert_or_update_show_output(
         out,
-        PROVE_RS_DIR / f'show/{src.stem}.{start_symbol}.cli-stats-leaves.expected',
+        PROVE_DIR / f'show/{src.stem}.{start_symbol}.cli-stats-leaves.expected',
         update=update_expected_output,
         path_replacements=_PATH_REPLACEMENTS,
     )
 
 
 def test_cli_info_snapshot(capsys: pytest.CaptureFixture[str], update_expected_output: bool) -> None:
-    smir_json = PROVE_RS_DIR / 'arith.smir.json'
+    smir_json = PROVE_DIR / 'arith.smir.json'
     smir_info = SMIRInfo.from_file(smir_json)
     # choose first few type ids deterministically
     chosen_tys = sorted(smir_info.types.keys())[:3]
@@ -139,12 +139,12 @@ def test_cli_info_snapshot(capsys: pytest.CaptureFixture[str], update_expected_o
     _kmir_info(info_opts)
     out = capsys.readouterr().out.rstrip()
     assert_or_update_show_output(
-        out, PROVE_RS_DIR / f'show/{smir_json.stem}.cli-info.expected', update=update_expected_output
+        out, PROVE_DIR / f'show/{smir_json.stem}.cli-info.expected', update=update_expected_output
     )
 
 
 def test_cli_link_counts_snapshot(tmp_path: Path, update_expected_output: bool) -> None:
-    smir1 = PROVE_RS_DIR / 'arith.smir.json'
+    smir1 = PROVE_DIR / 'arith.smir.json'
     smir2 = (Path(__file__).parent / 'data' / 'exec-smir' / 'arithmetic' / 'unary.smir.json').resolve(strict=True)
     output_file = tmp_path / 'linked.smir.json'
 
@@ -164,7 +164,7 @@ def test_cli_link_counts_snapshot(tmp_path: Path, update_expected_output: bool)
 
     assert_or_update_show_output(
         counts_text,
-        PROVE_RS_DIR / f'show/link.{smir1.stem}+{smir2.stem}.counts.expected',
+        PROVE_DIR / f'show/link.{smir1.stem}+{smir2.stem}.counts.expected',
         update=update_expected_output,
     )
 
@@ -172,7 +172,7 @@ def test_cli_link_counts_snapshot(tmp_path: Path, update_expected_output: bool)
 def test_cli_prune_snapshot(
     kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str], update_expected_output: bool
 ) -> None:
-    rs_file = PROVE_RS_DIR / 'assert-true.rs'
+    rs_file = PROVE_DIR / 'assert-true.rs'
     start_symbol = 'main'
     apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False)
 
@@ -180,7 +180,7 @@ def test_cli_prune_snapshot(
     _kmir_prune(prune_opts)
     out = capsys.readouterr().out.rstrip()
     assert_or_update_show_output(
-        out, PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-prune.expected', update=update_expected_output
+        out, PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-prune.expected', update=update_expected_output
     )
 
 
@@ -188,7 +188,7 @@ def test_cli_show_to_module(
     kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str], update_expected_output: bool
 ) -> None:
     """Test --to-module option with both K text and JSON output formats."""
-    rs_file = PROVE_RS_DIR / 'assert-true.rs'
+    rs_file = PROVE_DIR / 'assert-true.rs'
     start_symbol = 'main'
     apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False)
 
@@ -210,7 +210,7 @@ def test_cli_show_to_module(
     k_content = module_k_output.read_text()
     assert_or_update_show_output(
         k_content.rstrip(),
-        PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.k',
+        PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.k',
         update=update_expected_output,
     )
 
@@ -234,14 +234,14 @@ def test_cli_show_to_module(
     json.loads(json_content)
     assert_or_update_show_output(
         json_content.rstrip(),
-        PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.json',
+        PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.json',
         update=update_expected_output,
     )
 
 
 def test_cli_show_minimize_proof(kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str]) -> None:
     """Test --minimize-proof option."""
-    rs_file = PROVE_RS_DIR / 'symbolic-args-fail.rs'
+    rs_file = PROVE_DIR / 'symbolic-args-fail.rs'
     start_symbol = 'main'
     # Use limited depth to create a partial proof with intermediate nodes that can be minimized
     apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False, max_depth=5)
@@ -275,19 +275,19 @@ def test_cli_show_minimize_proof(kmir: KMIR, tmp_path: Path, capsys: pytest.Capt
     ), f'Minimization should not increase node count: {minimized_node_count} > {initial_node_count}'
 
 
-def test_cli_prove_rs_add_module(kmir: KMIR, tmp_path: Path) -> None:
-    """Test --add-module option for prove-rs using stored module files."""
+def test_cli_prove_add_module(kmir: KMIR, tmp_path: Path) -> None:
+    """Test --add-module option for prove using stored module files."""
     from kmir.kmir import KMIR
 
-    rs_file = PROVE_RS_DIR / 'assert-true.rs'
+    rs_file = PROVE_DIR / 'assert-true.rs'
     start_symbol = 'main'
 
     # Use the stored JSON module file generated by --to-module
-    stored_module_json = PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.json'
+    stored_module_json = PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.json'
     assert stored_module_json.exists(), f'Stored JSON module file not found: {stored_module_json}'
 
-    # Run prove-rs with --add-module and max_depth=1
-    opts_with_module = ProveRSOpts(
+    # Run prove with --add-module and max_depth=1
+    opts_with_module = ProveOpts(
         rs_file,
         proof_dir=tmp_path,
         smir=False,
@@ -295,7 +295,7 @@ def test_cli_prove_rs_add_module(kmir: KMIR, tmp_path: Path) -> None:
         max_depth=1,
         add_module=stored_module_json,
     )
-    proof_with_module = KMIR.prove_rs(opts_with_module)
+    proof_with_module = KMIR.prove_program(opts_with_module)
 
     # With depth=1, we should have 3 nodes: init, one step, target
     assert len(list(proof_with_module.kcfg.nodes)) == 3
@@ -307,17 +307,17 @@ def test_cli_break_on_function(
     """Test --break-on-function produces cut points at matching function and intrinsic calls."""
     from kmir.kmir import KMIR
 
-    rs_file = PROVE_RS_DIR / 'break-on-function.rs'
+    rs_file = PROVE_DIR / 'break-on-function.rs'
     start_symbol = 'main'
 
-    opts = ProveRSOpts(
+    opts = ProveOpts(
         rs_file,
         proof_dir=tmp_path,
         smir=False,
         start_symbol=start_symbol,
         break_on_function=['foo', 'black_box'],
     )
-    apr_proof = KMIR.prove_rs(opts)
+    apr_proof = KMIR.prove_program(opts)
     apr_proof.write_proof_data()
 
     show_opts = ShowOpts(
@@ -333,6 +333,6 @@ def test_cli_break_on_function(
 
     assert_or_update_show_output(
         out,
-        PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-break-on-function.expected',
+        PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-break-on-function.expected',
         update=update_expected_output,
     )
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 7e9b8cb0f..8c59cce9b 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -14,7 +14,7 @@
 
 from kmir.cargo import CargoProject
 from kmir.kmir import KMIR, KMIRAPRNodePrinter
-from kmir.options import ProveRSOpts, ShowOpts
+from kmir.options import ProveOpts, ShowOpts
 from kmir.parse.parser import Parser
 from kmir.smir import SMIRInfo
 from kmir.testing.fixtures import assert_or_update_show_output
@@ -25,9 +25,9 @@
     from kmir.parse.parser import JSON
 
 
-PROVE_RS_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
-PROVE_RS_FILES = list(PROVE_RS_DIR.glob('*.*'))
-PROVE_RS_START_SYMBOLS = {
+PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
+PROVE_FILES = list(PROVE_DIR.glob('*.*'))
+PROVE_START_SYMBOLS = {
     'symbolic-args-fail': ['main', 'eats_all_args'],
     'symbolic-structs-fail': ['eats_struct_args'],
     'unchecked_arithmetic': ['unchecked_add_i32', 'unchecked_sub_usize', 'unchecked_mul_isize'],
@@ -41,7 +41,7 @@
     'iter-eq-copied-take-dereftruncate': ['repro'],
     'spl-multisig-iter-eq-copied-next': ['repro'],
 }
-PROVE_RS_SHOW_SPECS = [
+PROVE_SHOW_SPECS = [
     'local-raw-fail',
     'interior-mut-fail',
     'interior-mut3-fail',
@@ -70,28 +70,28 @@
 
 @pytest.mark.parametrize(
     'rs_file',
-    PROVE_RS_FILES,
-    ids=[spec.stem for spec in PROVE_RS_FILES],
+    PROVE_FILES,
+    ids=[spec.stem for spec in PROVE_FILES],
 )
-def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
+def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
     should_fail = rs_file.stem.endswith('fail')
-    should_show = rs_file.stem in PROVE_RS_SHOW_SPECS
+    should_show = rs_file.stem in PROVE_SHOW_SPECS
     is_smir = rs_file.suffix == '.json'
 
     if update_expected_output and not should_show:
         pytest.skip()
 
-    prove_rs_opts = ProveRSOpts(rs_file, smir=is_smir)
+    prove_opts = ProveOpts(rs_file, smir=is_smir)
     printer = PrettyPrinter(kmir.definition)
     cterm_show = CTermShow(printer.print)
 
     start_symbols = ['main']
-    if rs_file.stem in PROVE_RS_START_SYMBOLS:
-        start_symbols = PROVE_RS_START_SYMBOLS[rs_file.stem]
+    if rs_file.stem in PROVE_START_SYMBOLS:
+        start_symbols = PROVE_START_SYMBOLS[rs_file.stem]
 
     for start_symbol in start_symbols:
-        prove_rs_opts.start_symbol = start_symbol
-        apr_proof = kmir.prove_rs(prove_rs_opts)
+        prove_opts.start_symbol = start_symbol
+        apr_proof = kmir.prove_program(prove_opts)
 
         if should_show:
             display_opts = ShowOpts(
@@ -100,7 +100,7 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No
             shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts))
             show_res = '\n'.join(shower.show(apr_proof))
             assert_or_update_show_output(
-                show_res, PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.expected', update=update_expected_output
+                show_res, PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected', update=update_expected_output
             )
 
         if not should_fail:
@@ -130,8 +130,8 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo
 
     # run proofs for all '<start-symbol>.expected' files (failing or not)
     for file in main_crate.parent.glob('*.expected'):
-        opts = ProveRSOpts(linked_file, smir=True, start_symbol=file.stem)
-        proof = kmir.prove_rs(opts)
+        opts = ProveOpts(linked_file, smir=True, start_symbol=file.stem)
+        proof = kmir.prove_program(opts)
 
         printer = PrettyPrinter(kmir.definition)
         cterm_show = CTermShow(printer.print)
@@ -408,9 +408,9 @@ def test_exec_smir(
 def test_prove_termination(test_data: tuple[str, Path], tmp_path: Path, kmir: KMIR) -> None:
     testname, smir_json = test_data
 
-    prove_rs_opts = ProveRSOpts(rs_file=smir_json, smir=True)
+    prove_opts = ProveOpts(rs_file=smir_json, smir=True)
 
-    proof = KMIR.prove_rs(prove_rs_opts)
+    proof = KMIR.prove_program(prove_opts)
     assert proof.passed
 
 
diff --git a/package/test-package.sh b/package/test-package.sh
index 98919d7ec..9e48d4e01 100755
--- a/package/test-package.sh
+++ b/package/test-package.sh
@@ -13,4 +13,4 @@ kmir --help
 #   && kmir run                                                             \
 # )
 
-# kmir prove-rs kmir/src/tests/integration/data/prove-rs/if.rs
+# kmir prove kmir/src/tests/integration/data/prove-rs/if.rs