diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index ca54f52cee..060a3bbce3 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -35,9 +35,9 @@ jobs:
 #      run: git clone https://github.com/0xPolygonHermez/pilcom.git  && cd pilcom && npm install
       run: git clone https://github.com/chriseth/pilcom.git -b main && cd pilcom && npm install
     - name: Build
-      run: cargo build
+      run: cargo build --features halo2
     - name: Run tests
-      run: PILCOM=$(pwd)/pilcom/ cargo test --verbose
+      run: PILCOM=$(pwd)/pilcom/ cargo test --features halo2 --verbose
     - name: Lint
       run: cargo clippy --all --all-features -- -D warnings
     - name: Format
@@ -66,6 +66,6 @@ jobs:
     - name: Install stdlib
       run: rustup component add rust-src --toolchain nightly-2023-01-03-x86_64-unknown-linux-gnu
     - name: Build
-      run: cargo build --release
+      run: cargo build --features halo2 --release
     - name: Run tests
-      run: cargo test -r --verbose -- --ignored --nocapture
+      run: cargo test -r --features halo2 --verbose -- --ignored --nocapture
diff --git a/Cargo.toml b/Cargo.toml
index 3ed85d7d3a..c77f0936af 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -10,7 +10,7 @@ members = [
     "pil_analyzer",
     "compiler",
     "pilgen",
-    "halo2"
+    "halo2",
 ]
 
 [patch."https://github.com/privacy-scaling-explorations/halo2.git"]
diff --git a/README.md b/README.md
index e76691db1a..7fbe582562 100644
--- a/README.md
+++ b/README.md
@@ -21,9 +21,9 @@ which is compiled to RISCV, then to powdr-asm and finally to PIL.
 
 *powdr*-PIL can be used to generate proofs using multiple backends, such as:
 
+- Halo2
 - eSTARKs: *powdr*-PIL is fully compatible with the eSTARKS backend from Polygon Hermez,
   although not yet fully integrated in an automatic way.
-- Halo2: ongoing work, should be ready soon.
 - Nova: ongoing work, should be ready after soon.
 - other STARKs: maybe?
 
diff --git a/compiler/Cargo.toml b/compiler/Cargo.toml
index de064f6507..37f0f548cc 100644
--- a/compiler/Cargo.toml
+++ b/compiler/Cargo.toml
@@ -14,3 +14,4 @@ executor = { path = "../executor" }
 pilgen = { path = "../pilgen" }
 pil_analyzer = { path = "../pil_analyzer" }
 halo2 = { path = "../halo2" }
+strum = { version = "0.24.1", features = ["derive"] }
\ No newline at end of file
diff --git a/compiler/src/backends.rs b/compiler/src/backends.rs
new file mode 100644
index 0000000000..0c0a5dda9e
--- /dev/null
+++ b/compiler/src/backends.rs
@@ -0,0 +1,7 @@
+use strum::{Display, EnumString, EnumVariantNames};
+
+#[derive(Clone, EnumString, EnumVariantNames, Display)]
+pub enum Backend {
+    #[strum(serialize = "halo2")]
+    Halo2,
+}
diff --git a/compiler/src/lib.rs b/compiler/src/lib.rs
index 4fae2f8be3..0d867bf2a2 100644
--- a/compiler/src/lib.rs
+++ b/compiler/src/lib.rs
@@ -1,13 +1,15 @@
 //! The main powdr lib, used to compile from assembly to PIL
 
+use std::ffi::OsStr;
 use std::fs;
 use std::io::BufWriter;
 use std::path::Path;
 use std::time::Instant;
-use std::{ffi::OsStr, io::Write};
 
+mod backends;
 mod verify;
-use halo2::prove_ast;
+
+pub use backends::Backend;
 use number::write_polys_file;
 use pil_analyzer::json_exporter;
 pub use verify::{compile_asm_string_temp, verify, verify_asm_string};
@@ -27,16 +29,16 @@ pub fn compile_pil_or_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     if file_name.ends_with(".asm") {
-        compile_asm(file_name, inputs, output_dir, force_overwrite, should_prove)
+        compile_asm(file_name, inputs, output_dir, force_overwrite, prove_with)
     } else {
         compile_pil(
             Path::new(file_name),
             output_dir,
             Some(inputs_to_query_callback(inputs)),
-            should_prove,
+            prove_with,
         );
     };
 }
@@ -49,14 +51,14 @@ pub fn compile_pil<T: FieldElement>(
     pil_file: &Path,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) -> bool {
     compile(
         &pil_analyzer::analyze(pil_file),
         pil_file.file_name().unwrap(),
         output_dir,
         query_callback,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -65,7 +67,7 @@ pub fn compile_pil_ast<T: FieldElement>(
     file_name: &OsStr,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) -> bool {
     // TODO exporting this to string as a hack because the parser
     // is tied into the analyzer due to imports.
@@ -74,7 +76,7 @@ pub fn compile_pil_ast<T: FieldElement>(
         file_name,
         output_dir,
         query_callback,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -85,7 +87,7 @@ pub fn compile_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let contents = fs::read_to_string(file_name).unwrap();
     compile_asm_string(
@@ -94,7 +96,7 @@ pub fn compile_asm<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -106,7 +108,7 @@ pub fn compile_asm_string<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let pil = pilgen::compile(Some(file_name), contents).unwrap_or_else(|err| {
         eprintln!("Error parsing .asm file:");
@@ -131,7 +133,7 @@ pub fn compile_asm_string<T: FieldElement>(
         pil_file_name.file_name().unwrap(),
         output_dir,
         Some(inputs_to_query_callback(inputs)),
-        should_prove,
+        prove_with,
     );
 }
 
@@ -140,7 +142,7 @@ fn compile<T: FieldElement>(
     file_name: &OsStr,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) -> bool {
     let mut success = true;
     let start = Instant::now();
@@ -162,8 +164,9 @@ fn compile<T: FieldElement>(
             &commits,
         );
         log::info!("Wrote commits.bin.");
-        if should_prove {
-            let proof = prove_ast(analyzed, constants, commits);
+        if let Some(Backend::Halo2) = prove_with {
+            use std::io::Write;
+            let proof = halo2::prove_ast(analyzed, constants, commits);
             let mut proof_file = fs::File::create(output_dir.join("proof.bin")).unwrap();
             let mut proof_writer = BufWriter::new(&mut proof_file);
             proof_writer.write_all(&proof).unwrap();
diff --git a/compiler/src/verify.rs b/compiler/src/verify.rs
index 0fd91b2395..1c2141952e 100644
--- a/compiler/src/verify.rs
+++ b/compiler/src/verify.rs
@@ -36,7 +36,7 @@ pub fn compile_asm_string_temp<T: FieldElement>(
                 _ => None,
             }
         }),
-        false,
+        None,
     ));
     (pil_file_name.to_string(), temp_dir)
 }
diff --git a/compiler/tests/pil.rs b/compiler/tests/pil.rs
index 8b88fb14e2..3a1039e4d7 100644
--- a/compiler/tests/pil.rs
+++ b/compiler/tests/pil.rs
@@ -12,7 +12,7 @@ pub fn verify_pil(file_name: &str, query_callback: Option<fn(&str) -> Option<Gol
         &input_file,
         &temp_dir,
         query_callback,
-        false,
+        None,
     ));
     compiler::verify(file_name, &temp_dir);
 }
diff --git a/executor/Cargo.toml b/executor/Cargo.toml
index ef70227987..c04b10bf51 100644
--- a/executor/Cargo.toml
+++ b/executor/Cargo.toml
@@ -12,6 +12,3 @@ parser = { path = "../parser" }
 pil_analyzer = { path = "../pil_analyzer" }
 rayon = "1.7.0"
 num-traits = "0.2.15"
-
-[dev-dependencies]
-mktemp = "0.5.0"
diff --git a/halo2/Cargo.toml b/halo2/Cargo.toml
index 9d232a6572..d0fb79a8d6 100644
--- a/halo2/Cargo.toml
+++ b/halo2/Cargo.toml
@@ -17,7 +17,4 @@ rand = "0.8.5"
 
 [dev-dependencies]
 executor = { path = "../executor" }
-pilgen = { path = "../pilgen" }
-
-[build-dependencies]
-lalrpop = "^0.19"
\ No newline at end of file
+pilgen = { path = "../pilgen" }
\ No newline at end of file
diff --git a/powdr_cli/src/main.rs b/powdr_cli/src/main.rs
index 3fb65050a1..9026763372 100644
--- a/powdr_cli/src/main.rs
+++ b/powdr_cli/src/main.rs
@@ -3,7 +3,7 @@
 mod util;
 
 use clap::{Parser, Subcommand};
-use compiler::compile_pil_or_asm;
+use compiler::{compile_pil_or_asm, Backend};
 use env_logger::{Builder, Target};
 use log::LevelFilter;
 use number::{Bn254Field, FieldElement, GoldilocksField};
@@ -57,10 +57,10 @@ enum Commands {
         #[arg(default_value_t = false)]
         force: bool,
 
-        /// Generate a halo2 proof
+        /// Generate a proof with a given backend
         #[arg(short, long)]
-        #[arg(default_value_t = false)]
-        prove: bool,
+        #[arg(value_parser = clap_enum_variants!(Backend))]
+        prove_with: Option<Backend>,
     },
     /// Compiles (no-std) rust code to riscv assembly, then to powdr assembly
     /// and finally to PIL and generates fixed and witness columns.
@@ -90,10 +90,10 @@ enum Commands {
         #[arg(default_value_t = false)]
         force: bool,
 
-        /// Generate a halo2 proof
+        /// Generate a proof with a given backend
         #[arg(short, long)]
-        #[arg(default_value_t = false)]
-        prove: bool,
+        #[arg(value_parser = clap_enum_variants!(Backend))]
+        prove_with: Option<Backend>,
     },
 
     /// Compiles riscv assembly to powdr assembly and then to PIL
@@ -123,10 +123,10 @@ enum Commands {
         #[arg(default_value_t = false)]
         force: bool,
 
-        /// Generate a halo2 proof.
+        /// Generate a proof with a given backend.
         #[arg(short, long)]
-        #[arg(default_value_t = false)]
-        prove: bool,
+        #[arg(value_parser = clap_enum_variants!(Backend))]
+        prove_with: Option<Backend>,
     },
 
     /// Apply the Halo2 workflow on an input file and prover values over the Bn254 field
@@ -175,7 +175,7 @@ fn main() {
             inputs,
             output_directory,
             force,
-            prove,
+            prove_with,
         } => call_with_field!(
             compile_rust,
             field,
@@ -183,7 +183,7 @@ fn main() {
             split_inputs(&inputs),
             Path::new(&output_directory),
             force,
-            prove
+            prove_with
         ),
         Commands::RiscvAsm {
             file,
@@ -191,7 +191,7 @@ fn main() {
             inputs,
             output_directory,
             force,
-            prove,
+            prove_with,
         } => call_with_field!(
             compile_riscv_asm,
             field,
@@ -200,7 +200,7 @@ fn main() {
             split_inputs(&inputs),
             Path::new(&output_directory),
             force,
-            prove
+            prove_with
         ),
         Commands::Reformat { file } => {
             let contents = fs::read_to_string(&file).unwrap();
@@ -215,7 +215,7 @@ fn main() {
             output_directory,
             inputs,
             force,
-            prove,
+            prove_with,
         } => call_with_field!(
             compile_pil_or_asm,
             field,
@@ -223,7 +223,7 @@ fn main() {
             split_inputs(&inputs),
             Path::new(&output_directory),
             force,
-            prove
+            prove_with
         ),
         Commands::Halo2MockProver { file, dir } => {
             halo2::mock_prove::<Bn254Field>(Path::new(&file), Path::new(&dir));
diff --git a/riscv/src/lib.rs b/riscv/src/lib.rs
index b7d3bf0f8d..0e6642396a 100644
--- a/riscv/src/lib.rs
+++ b/riscv/src/lib.rs
@@ -2,7 +2,7 @@
 
 use std::{collections::BTreeMap, path::Path, process::Command};
 
-use ::compiler::compile_asm_string;
+use ::compiler::{compile_asm_string, Backend};
 use mktemp::Temp;
 use std::fs;
 use walkdir::WalkDir;
@@ -22,7 +22,7 @@ pub fn compile_rust<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let riscv_asm = if file_name.ends_with("Cargo.toml") {
         compile_rust_crate_to_riscv_asm(file_name)
@@ -57,7 +57,7 @@ pub fn compile_rust<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -67,7 +67,7 @@ pub fn compile_riscv_asm_bundle<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let powdr_asm_file_name = output_dir.join(format!(
         "{}.asm",
@@ -96,7 +96,7 @@ pub fn compile_riscv_asm_bundle<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -108,7 +108,7 @@ pub fn compile_riscv_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let contents = fs::read_to_string(file_name).unwrap();
     compile_riscv_asm_bundle(
@@ -119,7 +119,7 @@ pub fn compile_riscv_asm<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }