chore: improve CLI help and clean up lints

Add clearer clap help text and CLI help assertions.\nDocument the full fmt/clippy/test verification flow in the project docs.\nRefactor STARK and runtime support code to satisfy rustfmt and clippy without changing behavior.

Author: AbdelStark

CLAUDE.md

@@ -19,9 +19,10 @@ llm-provable-computer is an implemented Rust workspace for a deterministic trans
 <status>
 - Milestone 1: complete.
 - Milestone 2: complete for the current proof scope.
-- Verified locally on 2026-03-18:
-  - `cargo test`
-  - `cargo test --features full`
+- Verified locally on 2026-03-19:
+  - `cargo fmt --all --check`
+  - `cargo clippy --all-targets --all-features -- -D warnings`
+  - `cargo test --all-features`
 - Current vanilla STARK scope:
   - supported: `NOP`, `LOADI`, `LOAD`, `STORE`, `PUSH`, `POP`, `ADD`, `ADDM`, `SUB`, `SUBM`, `MUL`, `MULM`, `CALL`, `RET`, `JMP`, `JZ`, `JNZ`, `HALT`
   - rejected: softmax and hard-softmax proof paths, bitwise instructions, compare instructions, non-halted public claims, public claims with `carry_flag = true`
@@ -36,7 +37,6 @@ Cargo.toml
 Cargo.lock
 README.md
 CLAUDE.md
-LICENSE
 src/
   assembly.rs           # .tvm parser, directives, labels
   compiler.rs           # ProgramCompiler
@@ -74,14 +74,16 @@ scripts/
 | Inventory files | `rg --files` | Fastest repo scan |
 | Check repo state | `git status --short` | Separate your edits from unrelated files |
 | Run default suite | `cargo test` | Core milestone-1 and milestone-2 validation |
-| Run full engine suite | `cargo test --features full` | Burn + ONNX + Python validator + CLI workflow |
+| Check formatting | `cargo fmt --all --check` | Matches CI-ready rustfmt output |
+| Run strict lint pass | `cargo clippy --all-targets --all-features -- -D warnings` | Keep the full tree warning-free |
+| Run full engine suite | `cargo test --all-features` | Burn + ONNX + Python validator + CLI workflow |
 | Run a program | `cargo run --bin tvm -- programs/fibonacci.tvm` | Shortcut for `tvm run` |
 | Trace execution | `cargo run --bin tvm -- run programs/counter.tvm --trace` | Emits trace and summary |
 | Verify transformer vs native | `cargo run --bin tvm -- run programs/fibonacci.tvm --verify-native` | Lockstep comparison |
 | Verify all engines | `cargo run --features full --bin tvm -- run programs/fibonacci.tvm --verify-all` | Transformer + native + Burn + ONNX |
 | Create a proof | `cargo run --bin tvm -- prove-stark programs/fibonacci.tvm -o /tmp/fib.proof.json` | Uses current vanilla STARK path |
 | Verify a proof | `cargo run --bin tvm -- verify-stark /tmp/fib.proof.json` | Re-checks a saved proof |
-| Review doc drift | `git diff -- README.md SPEC.md IMPLEMENTATION_PLAN.md CLAUDE.md` | Use before finishing doc/context work |
+| Review doc drift | `git diff -- README.md CLAUDE.md docs/` | Use before finishing doc/context work |
 </commands>
 
 <workflows>
@@ -94,8 +96,8 @@ scripts/
 
   <proof_change>
   1. Read `src/proof.rs` and `src/vanillastark/**`.
-  2. Update support and limitation language in `SPEC.md` and `README.md`.
-  3. Re-run at least `cargo test` and, when Burn or ONNX paths are affected, `cargo test --features full`.
+  2. Update support and limitation language in `README.md`, `CLAUDE.md`, and matching files under `docs/`.
+  3. Re-run at least `cargo test` and, when Burn or ONNX paths are affected, `cargo test --all-features`.
   </proof_change>
 
   <engine_change>
@@ -123,7 +125,7 @@ scripts/
   |---------|--------------|-----|
   | `prove-stark` rejects a program | Unsupported instruction, attention mode, or claim shape | Check `src/proof.rs::validate_proof_inputs` and the carry/halted restrictions |
   | Burn or ONNX commands are unavailable | Missing feature flag | Re-run with `--features burn-model`, `--features onnx-export`, or `--features full` |
-  | Docs mention WASM compilation as current behavior | Stale pre-implementation text | Prefer `SPEC.md` and the source tree over old planning language |
+  | Docs mention WASM compilation as current behavior | Stale pre-implementation text | Prefer `README.md`, `CLAUDE.md`, and the source tree over old planning language |
   | An engine mismatch appears during verification | Trace divergence across runtimes | Inspect `ExecutionTraceEntry` output and compare instruction/state pairs |
   </known_issues>
 </troubleshooting>

README.md

@@ -304,6 +304,21 @@ cargo test --features full    # Everything
 cargo bench                   # Hull + STARK benchmarks
 ```
 
+## Development Checks
+
+```bash
+cargo fmt --all --check
+cargo clippy --all-targets --all-features -- -D warnings
+cargo test --all-features
+```
+
+The CLI is self-documenting:
+
+```bash
+cargo run --bin tvm -- --help
+cargo run --bin tvm -- run --help
+```
+
 ---
 
 ## Repository Structure

benches/hull_benchmark.rs

@@ -1,6 +1,6 @@
 use criterion::{black_box, criterion_group, criterion_main, BenchmarkId, Criterion};
-use rand::{rngs::StdRng, Rng, SeedableRng};
 use llm_provable_computer::HullKvCache;
+use rand::{rngs::StdRng, Rng, SeedableRng};
 
 fn bench_query_scaling(c: &mut Criterion) {
     let mut group = c.benchmark_group("hull_query_vs_bruteforce");

src/bin/tvm.rs

@@ -26,87 +26,120 @@ use llm_provable_computer::{BurnExecutionRuntime, BurnTransformerVm};
 type CliBurnBackend = NdArray<f64>;
 
 #[derive(Debug, Parser)]
-#[command(name = "tvm", about = "Run deterministic llm-provable-computer programs.")]
+#[command(
+    name = "tvm",
+    about = "Run deterministic llm-provable-computer programs."
+)]
 struct Cli {
     #[command(subcommand)]
     command: Command,
 }
 
 #[derive(Debug, Subcommand)]
 enum Command {
+    /// Run a program and print the final machine state.
     Run {
+        /// Path to the source `.tvm` program.
         program: PathBuf,
+        /// Maximum number of execution steps before stopping.
         #[arg(long, default_value_t = 512)]
         max_steps: usize,
+        /// Emit the full step-by-step execution trace.
         #[arg(long)]
         trace: bool,
+        /// Number of transformer layers to distribute instructions across.
         #[arg(long, default_value_t = 1)]
         layers: usize,
+        /// Execution backend to use for the run.
         #[arg(
             long,
             default_value = "transformer",
             value_parser = parse_execution_engine
         )]
         engine: CliExecutionEngine,
+        /// Verify the transformer runtime against the native interpreter.
         #[arg(long)]
         verify_native: bool,
+        /// Verify the transformer and native runtimes against Burn.
         #[arg(long)]
         verify_burn: bool,
+        /// Verify the transformer and native runtimes against ONNX.
         #[arg(long)]
         verify_onnx: bool,
+        /// Verify all available runtimes in lockstep.
         #[arg(long, conflicts_with_all = ["verify_native", "verify_burn", "verify_onnx"])]
         verify_all: bool,
+        /// Attention mode to use for memory reads.
         #[arg(
             long,
             default_value = "average-hard",
             value_parser = parse_attention_mode
         )]
         attention_mode: Attention2DMode,
     },
+    /// Run the interactive terminal viewer for a program.
     Tui {
+        /// Path to the source `.tvm` program.
         program: PathBuf,
+        /// Maximum number of execution steps before stopping.
         #[arg(long, default_value_t = 512)]
         max_steps: usize,
+        /// Number of transformer layers to distribute instructions across.
         #[arg(long, default_value_t = 1)]
         layers: usize,
+        /// UI refresh interval in milliseconds.
         #[arg(long, default_value_t = 60)]
         tick_ms: u64,
+        /// Attention mode to use for memory reads.
         #[arg(
             long,
             default_value = "average-hard",
             value_parser = parse_attention_mode
         )]
         attention_mode: Attention2DMode,
     },
+    /// Export the compiled program as per-instruction ONNX graphs.
     ExportOnnx {
+        /// Path to the source `.tvm` program.
         program: PathBuf,
+        /// Directory where ONNX models and metadata will be written.
         #[arg(short = 'o', long = "output-dir")]
         output_dir: PathBuf,
+        /// Number of transformer layers to distribute instructions across.
         #[arg(long, default_value_t = 1)]
         layers: usize,
+        /// Attention mode to use for memory reads.
         #[arg(
             long,
             default_value = "average-hard",
             value_parser = parse_attention_mode
         )]
         attention_mode: Attention2DMode,
     },
+    /// Produce a STARK proof for a supported execution.
     ProveStark {
+        /// Path to the source `.tvm` program.
         program: PathBuf,
+        /// File where the serialized proof JSON will be written.
         #[arg(short = 'o', long = "output")]
         output: PathBuf,
+        /// Maximum number of execution steps before stopping.
         #[arg(long, default_value_t = 512)]
         max_steps: usize,
+        /// Number of transformer layers to distribute instructions across.
         #[arg(long, default_value_t = 1)]
         layers: usize,
+        /// Attention mode to use for memory reads.
         #[arg(
             long,
             default_value = "average-hard",
             value_parser = parse_attention_mode
         )]
         attention_mode: Attention2DMode,
     },
+    /// Verify a previously generated STARK proof.
     VerifyStark {
+        /// Path to the serialized proof JSON file.
         proof: PathBuf,
     },
 }
@@ -137,6 +170,20 @@ struct EngineRunOutput {
     events: Vec<ExecutionTraceEntry>,
 }
 
+#[derive(Debug, Clone)]
+struct RunCommandOptions {
+    program: PathBuf,
+    max_steps: usize,
+    trace: bool,
+    layers: usize,
+    engine: CliExecutionEngine,
+    verify_native: bool,
+    verify_burn: bool,
+    verify_onnx: bool,
+    verify_all: bool,
+    attention_mode: Attention2DMode,
+}
+
 #[cfg(feature = "onnx-export")]
 struct ScopedTempDir {
     path: PathBuf,
@@ -190,8 +237,8 @@ fn run() -> llm_provable_computer::Result<()> {
             verify_onnx,
             verify_all,
             attention_mode,
-        } => run_program_command(
-            &program,
+        } => run_program_command(RunCommandOptions {
+            program,
             max_steps,
             trace,
             layers,
@@ -201,7 +248,7 @@ fn run() -> llm_provable_computer::Result<()> {
             verify_onnx,
             verify_all,
             attention_mode,
-        )?,
+        })?,
         Command::Tui {
             program,
             max_steps,
@@ -231,25 +278,18 @@ fn run() -> llm_provable_computer::Result<()> {
     Ok(())
 }
 
-fn run_program_command(
-    program: &Path,
-    max_steps: usize,
-    trace: bool,
-    layers: usize,
-    engine: CliExecutionEngine,
-    verify_native: bool,
-    verify_burn: bool,
-    verify_onnx: bool,
-    verify_all: bool,
-    attention_mode: Attention2DMode,
-) -> llm_provable_computer::Result<()> {
-    let model = compile_model(program, layers, attention_mode.clone())?;
-    let executed = execute_engine(&model, engine, max_steps)?;
+fn run_program_command(options: RunCommandOptions) -> llm_provable_computer::Result<()> {
+    let model = compile_model(
+        &options.program,
+        options.layers,
+        options.attention_mode.clone(),
+    )?;
+    let executed = execute_engine(&model, options.engine, options.max_steps)?;
 
-    print_execution_summary(program, engine, &model, &executed.result);
+    print_execution_summary(&options.program, options.engine, &model, &executed.result);
 
-    if verify_native {
-        let comparison = verify_model_against_native(model.clone(), max_steps)?;
+    if options.verify_native {
+        let comparison = verify_model_against_native(model.clone(), options.max_steps)?;
         println!("verified_against_native: true");
         println!("verified_steps: {}", comparison.checked_steps);
         println!(
@@ -262,8 +302,8 @@ fn run_program_command(
         );
     }
 
-    if verify_burn {
-        let verification = verify_burn_engines(&model, max_steps)?;
+    if options.verify_burn {
+        let verification = verify_burn_engines(&model, options.max_steps)?;
         print_verification_summary(
             "verified_against_burn",
             "verified_burn",
@@ -272,8 +312,8 @@ fn run_program_command(
         );
     }
 
-    if verify_onnx {
-        let verification = verify_onnx_engines(&model, max_steps)?;
+    if options.verify_onnx {
+        let verification = verify_onnx_engines(&model, options.max_steps)?;
         print_verification_summary(
             "verified_against_onnx",
             "verified_onnx",
@@ -282,8 +322,8 @@ fn run_program_command(
         );
     }
 
-    if verify_all {
-        let verification = verify_all_engines(&model, max_steps)?;
+    if options.verify_all {
+        let verification = verify_all_engines(&model, options.max_steps)?;
         print_verification_summary(
             "verified_all",
             "verified_all",
@@ -292,7 +332,7 @@ fn run_program_command(
         );
     }
 
-    if trace {
+    if options.trace {
         print_trace(&executed.trace, &executed.events);
     }
 

src/burn_model.rs

@@ -222,7 +222,7 @@ impl<B: Backend> BurnTransformerVm<B> {
         let mut banks = vec![vec![None; model.program().len()]; model.config().num_layers];
         let mut layer_for_pc = Vec::with_capacity(model.program().len());
 
-        for pc in 0..model.program().len() {
+        for (pc, _) in model.program().instructions().iter().enumerate() {
             let (compiled, layer_idx) = model.compiled_instruction(pc as u8)?;
             layer_for_pc.push(layer_idx);
             banks[layer_idx][pc] = Some(BurnCompiledInstruction::from_compiled(compiled, device));

src/onnx_export.rs

@@ -440,7 +440,8 @@ fn export_instruction_onnx(
     model.domain = "com.llm_provable_computer".to_string();
     model.model_version = FORMAT_VERSION as i64;
     model.doc_string =
-        "Per-instruction llm-provable-computer feed-forward export with explicit flag outputs".to_string();
+        "Per-instruction llm-provable-computer feed-forward export with explicit flag outputs"
+            .to_string();
     model.graph = MessageField::some(graph);
     model
 }

src/proof.rs

@@ -418,19 +418,20 @@ impl VmAir {
             }
         }
 
-        let mut constraints = Vec::new();
-        constraints.push(valid_pc);
-        constraints.push(valid_sp);
-        constraints.push(current_zero.clone() * (current_zero.clone() - one.clone()));
-        constraints.push(current[HALTED].clone());
-        constraints.push(current[CARRY].clone());
-        constraints.push(next_pc - expected_next_pc);
-        constraints.push(next_acc.clone() - expected_next_acc);
-        constraints.push(next_sp - expected_next_sp);
-        constraints.push(next_halted - expected_next_halted);
-        constraints.push(next_carry);
-        constraints.push(next_acc.clone() * next_acc_inv - (one.clone() - next_zero.clone()));
-        constraints.push(next_zero * next_acc);
+        let mut constraints = vec![
+            valid_pc,
+            valid_sp,
+            current_zero.clone() * (current_zero.clone() - one.clone()),
+            current[HALTED].clone(),
+            current[CARRY].clone(),
+            next_pc - expected_next_pc,
+            next_acc.clone() - expected_next_acc,
+            next_sp - expected_next_sp,
+            next_halted - expected_next_halted,
+            next_carry,
+            next_acc.clone() * next_acc_inv - (one.clone() - next_zero.clone()),
+            next_zero * next_acc,
+        ];
 
         if !self.layout.memory_size.is_zero() {
             constraints.push(