diff --git a/Ix/Cli/HashCmd.lean b/Ix/Cli/HashCmd.lean
new file mode 100644
index 00000000..e8f5bb92
--- /dev/null
+++ b/Ix/Cli/HashCmd.lean
@@ -0,0 +1,17 @@
+import Cli
+
+def runHash (p : Cli.Parsed) : IO UInt32 := do
+  let input   : String       := p.positionalArg! "input" |>.as! String
+  IO.println <| "Input: " ++ input
+  return 0
+
+def hashCmd : Cli.Cmd := `[Cli|
+  hash VIA runHash;
+  "Hashes a given Lean source file"
+
+  FLAGS:
+    e, "example"   : String; "Example flag"
+
+  ARGS:
+    input  : String; "Source file input"
+]
diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean
new file mode 100644
index 00000000..a1f40698
--- /dev/null
+++ b/Ix/Cli/ProveCmd.lean
@@ -0,0 +1,17 @@
+import Cli
+
+def runProve (p : Cli.Parsed) : IO UInt32 := do
+  let input   : String       := p.positionalArg! "input" |>.as! String
+  IO.println <| "Input: " ++ input
+  return 0
+
+def proveCmd : Cli.Cmd := `[Cli|
+  prove VIA runProve;
+  "Generates a ZK proof of a given Lean source file"
+
+  FLAGS:
+    e, "example"   : String; "Example flag"
+
+  ARGS:
+   input  : String; "Source file input"
+]
diff --git a/Main.lean b/Main.lean
index adc9b301..9f1db352 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,4 +1,20 @@
-import Ix
+import Ix.Cli.ProveCmd
+import Ix.Cli.HashCmd
 
-def main (args : List String) : IO Unit :=
-  IO.println s!"Hello, {args}!"
+def VERSION : String :=
+  s!"{Lean.versionString}|0.0.1"
+
+def ixCmd : Cli.Cmd := `[Cli|
+  ix NOOP; [VERSION]
+  "A tool for generating content-addressed ZK proofs of Lean 4 code"
+
+  SUBCOMMANDS:
+    proveCmd;
+    hashCmd
+]
+
+def main (args : List String) : IO UInt32 := do
+  if args.isEmpty then
+    ixCmd.printHelp
+    return 0
+  ixCmd.validate args
diff --git a/lake-manifest.json b/lake-manifest.json
index 12ad7779..582f4664 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/argumentcomputer/LSpec",
+ [{"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "efa5aa20504b88e2826032ddaa606c7965ec9467",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "efa5aa20504b88e2826032ddaa606c7965ec9467",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
diff --git a/lakefile.lean b/lakefile.lean
index 19e83ec0..ec7c1d68 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,6 +13,9 @@ lean_exe ix where
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
 
+require Cli from git
+  "https://github.com/leanprover/lean4-cli" @ "efa5aa20504b88e2826032ddaa606c7965ec9467"
+
 section Tests
 
 lean_exe Tests.Blake3