diff --git a/src/sat/Proof_dummy.ml b/src/sat/Proof_dummy.ml
new file mode 100644
index 00000000..5cfb08b9
--- /dev/null
+++ b/src/sat/Proof_dummy.ml
@@ -0,0 +1,22 @@
+
+module Make(Lit : sig type t end)
+  : Solver_intf.PROOF
+    with type lit = Lit.t
+     and type t = unit
+     and type proof_step = unit
+= struct
+  type lit = Lit.t
+  type t = unit
+  type proof_step = unit
+  type proof_rule = t -> proof_step
+
+  module Step_vec = Vec_unit
+
+  let enabled (_pr:t) = false
+  let del_clause _ _ (_pr:t) = ()
+
+  let emit_redundant_clause _ ~hyps:_ _ = ()
+  let emit_input_clause _ _ = ()
+  let emit_unsat _ _ = ()
+  let emit_unsat_core _ (_pr:t) = ()
+end
diff --git a/src/sat/Proof_dummy.mli b/src/sat/Proof_dummy.mli
new file mode 100644
index 00000000..488ebab6
--- /dev/null
+++ b/src/sat/Proof_dummy.mli
@@ -0,0 +1,9 @@
+
+(** Dummy proof module that does nothing. *)
+
+module Make(Lit : sig type t end) : sig
+  include Solver_intf.PROOF
+    with type lit = Lit.t
+     and type t = unit
+     and type proof_step = unit
+end
diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml
index ccbeda03..fc956231 100644
--- a/src/sat/Sidekick_sat.ml
+++ b/src/sat/Sidekick_sat.ml
@@ -32,3 +32,6 @@ exception No_proof = Solver_intf.No_proof
 module Solver = Solver
 module Make_cdcl_t = Solver.Make_cdcl_t
 module Make_pure_sat = Solver.Make_pure_sat
+
+(** Module for dummy proofs based on unit *)
+module Proof_dummy = Proof_dummy