diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index a5d6eafc..06334858 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -40,11 +40,18 @@ module type Backend = sig
     backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
 end
 
-module type SolverIo = sig
-  type vc_encoding
+module type BackendIO = sig
+  val init_backend : unit -> unit
 
   type backend_context
 
+  val make_context : decl_ctx -> typ Pos.marked VarMap.t -> backend_context
+
+  type vc_encoding
+
+  val translate_expr :
+    backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
+
   type model
 
   type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
@@ -58,11 +65,17 @@ module type SolverIo = sig
     Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
 end
 
-module MakeSolverIO (B : Backend) = struct
-  type vc_encoding = B.vc_encoding
+module MakeBackendIO (B : Backend) = struct
+  let init_backend = B.init_backend
 
   type backend_context = B.backend_context
 
+  let make_context = B.make_context
+
+  type vc_encoding = B.vc_encoding
+
+  let translate_expr = B.translate_expr
+
   type model = B.model
 
   type vc_encoding_result = Success of B.vc_encoding * B.backend_context | Fail of string
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index b3fe09e8..6fe134ed 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -40,11 +40,19 @@ module type Backend = sig
     backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
 end
 
-module type SolverIo = sig
-  type vc_encoding
+module type BackendIO = sig
+  val init_backend : unit -> unit
 
   type backend_context
 
+  val make_context :
+    Dcalc.Ast.decl_ctx -> Dcalc.Ast.typ Utils.Pos.marked Dcalc.Ast.VarMap.t -> backend_context
+
+  type vc_encoding
+
+  val translate_expr :
+    backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
+
   type model
 
   type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
@@ -58,8 +66,8 @@ module type SolverIo = sig
     Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
 end
 
-module MakeSolverIO : functor (B : Backend) ->
-  SolverIo
+module MakeBackendIO : functor (B : Backend) ->
+  BackendIO
     with type vc_encoding = B.vc_encoding
      and type backend_context = B.backend_context
      and type model = B.model
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 3df570bc..881d94d2 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -21,15 +21,15 @@ let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verificati
     unit =
   (* Right now we only use the Z3 backend but the functorial interface should make it easy to mix
      and match different proof backends. *)
-  Z3backend.Backend.init_backend ();
+  Z3backend.Io.init_backend ();
   let z3_vcs =
     List.map
       (fun vc ->
         ( vc,
           try
             let ctx, z3_vc =
-              Z3backend.Backend.translate_expr
-                (Z3backend.Backend.make_context decl_ctx
+              Z3backend.Io.translate_expr
+                (Z3backend.Io.make_context decl_ctx
                    (VarMap.union
                       (fun _ _ _ ->
                         failwith "[Proof encoding]: A Variable cannot be both free and bound")
diff --git a/compiler/verification/z3backend.ml b/compiler/verification/z3backend.ml
index d1e89c5a..0dfe3237 100644
--- a/compiler/verification/z3backend.ml
+++ b/compiler/verification/z3backend.ml
@@ -601,4 +601,4 @@ module Backend = struct
     }
 end
 
-module Io = Io.MakeSolverIO (Backend)
+module Io = Io.MakeBackendIO (Backend)
diff --git a/compiler/verification/z3backend.mli b/compiler/verification/z3backend.mli
index d39adacc..6bc1eb04 100644
--- a/compiler/verification/z3backend.mli
+++ b/compiler/verification/z3backend.mli
@@ -14,10 +14,4 @@
 
 (** Interfacing with the Z3 SMT solver *)
 
-module Backend : Io.Backend
-
-module Io :
-  Io.SolverIo
-    with type backend_context = Backend.backend_context
-     and type model = Backend.model
-     and type vc_encoding = Backend.vc_encoding
+module Io : Io.BackendIO