diff --git a/doc/extensions.md b/doc/extensions.md
new file mode 100644
index 000000000..78133b772
--- /dev/null
+++ b/doc/extensions.md
@@ -0,0 +1,25 @@
+# User-defined builtins
+
+Dolmen supports extensions through the form of user-defined builtins; see the
+`abs_real` and `abs_real_split` plugins.
+
+User-defined builtins can be added to the extensible `Builtin` type in
+`Dolmen.Std.Builtin.t`.
+
+Builtins need to be registered with the typer using `Dolmen_loop.Typer.Ext`,
+and they optionally need to be registered with the model evaluation mechanism
+(if they are to be used with model verification) using `Dolmen_model.Env.Ext`.
+
+The `dolmen` command-line tool looks up user-defined extensions using the Dune
+plugin mechanism. A plugin named `plugin.typing` will be picked up when
+`--ext plugin` or `--ext plugin.typing` is provided on the command-line, and
+the plugin must register a typing extension named `"plugin"` using
+`Dolmen_loop.Typer.Ext.create`. A plugin named `plugin.model` will be picked up
+when `--ext plugin` or `--ext plugin.model` is provided on the command-line and
+the plugin must register a model extension named `"plugin"` using
+`Dolmen_model.Env.Ext.create`. A plugin named `plugin` (without dots) will be
+picked up when either of the above command line flags is provided, and must
+provide both a typing and model extension.
+
+*Note*: Model extensions are only used (and their existence checked) if the
+user provides the `--check-model` flag.
diff --git a/dolmen_bin.opam b/dolmen_bin.opam
index 8a91c564b..06fedac2d 100644
--- a/dolmen_bin.opam
+++ b/dolmen_bin.opam
@@ -15,6 +15,7 @@ depends: [
   "dolmen_loop" {= version }
   "dolmen_model" {= version }
   "dune" { >= "3.0" }
+  "dune-site" { >= "3.0" }
   "fmt"
   "cmdliner" { >= "1.1.0" }
   "odoc" { with-doc }
diff --git a/dune-project b/dune-project
index 7a21df0b7..dbb474e7e 100644
--- a/dune-project
+++ b/dune-project
@@ -2,4 +2,24 @@
 (name dolmen)
 (using mdx 0.2)
 (using menhir 2.0)
+(using dune_site 0.1)
 (implicit_transitive_deps true)
+
+(package
+  (name dolmen)
+  (sites (lib plugins)))
+
+(package
+  (name dolmen_type))
+
+(package
+  (name dolmen_loop))
+
+(package
+  (name dolmen_model))
+
+(package
+  (name dolmen_bin))
+
+(package
+  (name dolmen_lsp))
diff --git a/examples/extensions/abs_real/README.md b/examples/extensions/abs_real/README.md
new file mode 100644
index 000000000..7162d9469
--- /dev/null
+++ b/examples/extensions/abs_real/README.md
@@ -0,0 +1,5 @@
+# `abs_real` plugin
+
+This is an example plugin adding support for an `abs_real` function. This
+plugin implements both the typing and model extensions for the `abs_real`
+function in the same Dune plugin.
diff --git a/examples/extensions/abs_real/abs_real.ml b/examples/extensions/abs_real/abs_real.ml
new file mode 100644
index 000000000..ac252b715
--- /dev/null
+++ b/examples/extensions/abs_real/abs_real.ml
@@ -0,0 +1,49 @@
+type _ Dolmen.Std.Builtin.t += Abs_real
+
+module Type = Dolmen_loop.Typer.T
+module Ty = Dolmen.Std.Expr.Ty
+module Term = Dolmen.Std.Expr.Term
+module Builtin = Dolmen.Std.Builtin
+module Base = Dolmen_type.Base
+
+module Const = struct
+  let mk' ?pos ?name ?builtin ?tags cname vars args ret =
+    let ty = Ty.pi vars (Ty.arrow args ret) in
+    Dolmen.Std.Expr.Id.mk ?pos ?name ?builtin ?tags
+      (Dolmen.Std.Path.global cname) ty
+
+  module Real = struct
+    (* NB: Use [Dolmen.Std.Expr.with_cache] for parameterized builtins. *)
+    let abs =
+      mk' ~builtin:Abs_real "abs_real"
+        [] [Ty.real] Ty.real
+  end
+end
+
+let abs_real x = Term.apply_cst Const.Real.abs [] [x]
+
+let builtins _lang env s =
+  match s with
+  | Type.Id { ns = Term ; name = Simple "abs_real" } ->
+    Type.builtin_term (Base.term_app1 (module Type) env s abs_real)
+  | _ -> `Not_found
+
+let typing_ext =
+  Dolmen_loop.Typer.Ext.create ~name:"abs_real" ~builtins
+
+module B = Dolmen.Std.Builtin
+module Fun = Dolmen_model.Fun
+
+let real = Dolmen_model.Real.mk
+let of_real = Dolmen_model.Real.get
+
+let abs_real ~cst =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> real (Q.abs (of_real x))))
+
+let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | Abs_real -> abs_real ~cst
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Env.Ext.create ~name:"abs_real" ~builtins
diff --git a/examples/extensions/abs_real/dune b/examples/extensions/abs_real/dune
new file mode 100644
index 000000000..8b6127197
--- /dev/null
+++ b/examples/extensions/abs_real/dune
@@ -0,0 +1,10 @@
+(library
+  (public_name dolmen-extensions-abs-real.plugin)
+  (name abs_real)
+  (modules abs_real)
+  (libraries dolmen_model))
+
+(plugin
+  (name abs_real)
+  (libraries dolmen-extensions-abs-real.plugin)
+  (site (dolmen plugins)))
diff --git a/examples/extensions/abs_real/dune-project b/examples/extensions/abs_real/dune-project
new file mode 100644
index 000000000..7bb297bf8
--- /dev/null
+++ b/examples/extensions/abs_real/dune-project
@@ -0,0 +1,8 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(generate_opam_files false)
+
+(package
+  (name dolmen-extensions-abs-real)
+  (depopts dolmen_type dolmen_loop dolmen_model))
diff --git a/examples/extensions/abs_real_split/README.md b/examples/extensions/abs_real_split/README.md
new file mode 100644
index 000000000..824414119
--- /dev/null
+++ b/examples/extensions/abs_real_split/README.md
@@ -0,0 +1,8 @@
+# `abs_real_split` plugin
+
+This is an example plugin adding support for an `abs_real` function. This
+plugin implements the typing and model extensions for the `abs_real` function
+in separate Dune plugins.
+
+This is more complex than implementing `abs_real` as a single plugin, but
+allows using the typing extension without a dependency on `dolmen_model`.
diff --git a/examples/extensions/abs_real_split/builtin.ml b/examples/extensions/abs_real_split/builtin.ml
new file mode 100644
index 000000000..86cdb8a64
--- /dev/null
+++ b/examples/extensions/abs_real_split/builtin.ml
@@ -0,0 +1 @@
+type _ Dolmen.Std.Builtin.t += Abs_real
\ No newline at end of file
diff --git a/examples/extensions/abs_real_split/dune b/examples/extensions/abs_real_split/dune
new file mode 100644
index 000000000..fb4b7725e
--- /dev/null
+++ b/examples/extensions/abs_real_split/dune
@@ -0,0 +1,27 @@
+(library
+  (name abs_real_split)
+  (modules builtin)
+  (libraries dolmen)
+  (package dolmen-extensions-abs-real-split))
+
+(library
+  (public_name dolmen-extensions-abs-real-split.typing)
+  (name typing)
+  (modules typing)
+  (libraries dolmen_loop abs_real_split))
+
+(library
+  (public_name dolmen-extensions-abs-real-split.model)
+  (name model)
+  (modules model)
+  (libraries dolmen_model abs_real_split))
+
+(plugin
+  (name abs_real_split.typing)
+  (libraries dolmen-extensions-abs-real-split.typing)
+  (site (dolmen plugins)))
+
+(plugin
+  (name abs_real_split.model)
+  (libraries dolmen-extensions-abs-real-split.model)
+  (site (dolmen plugins)))
diff --git a/examples/extensions/abs_real_split/dune-project b/examples/extensions/abs_real_split/dune-project
new file mode 100644
index 000000000..ffda1f523
--- /dev/null
+++ b/examples/extensions/abs_real_split/dune-project
@@ -0,0 +1,8 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(generate_opam_files false)
+
+(package
+  (name dolmen-extensions-abs-real-split)
+  (depopts dolmen_type dolmen_loop dolmen_model))
diff --git a/examples/extensions/abs_real_split/model.ml b/examples/extensions/abs_real_split/model.ml
new file mode 100644
index 000000000..b404beba6
--- /dev/null
+++ b/examples/extensions/abs_real_split/model.ml
@@ -0,0 +1,16 @@
+module B = Dolmen.Std.Builtin
+module Fun = Dolmen_model.Fun
+
+let real = Dolmen_model.Real.mk
+let of_real = Dolmen_model.Real.get
+
+let abs_real ~cst =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> real (Q.abs (of_real x))))
+
+let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | Abs_real_split.Builtin.Abs_real -> abs_real ~cst
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Env.Ext.create ~name:"abs_real_split" ~builtins
diff --git a/examples/extensions/abs_real_split/typing.ml b/examples/extensions/abs_real_split/typing.ml
new file mode 100644
index 000000000..538492ba5
--- /dev/null
+++ b/examples/extensions/abs_real_split/typing.ml
@@ -0,0 +1,30 @@
+module Type = Dolmen_loop.Typer.T
+module Ty = Dolmen.Std.Expr.Ty
+module Term = Dolmen.Std.Expr.Term
+module Builtin = Dolmen.Std.Builtin
+module Base = Dolmen_type.Base
+
+module Const = struct
+  let mk' ?pos ?name ?builtin ?tags cname vars args ret =
+    let ty = Ty.pi vars (Ty.arrow args ret) in
+    Dolmen.Std.Expr.Id.mk ?pos ?name ?builtin ?tags
+      (Dolmen.Std.Path.global cname) ty
+
+  module Real = struct
+    (* NB: Use [Dolmen.Std.Expr.with_cache] for parameterized builtins. *)
+    let abs =
+      mk' ~builtin:Abs_real_split.Builtin.Abs_real "abs_real"
+        [] [Ty.real] Ty.real
+  end
+end
+
+let abs_real x = Term.apply_cst Const.Real.abs [] [x]
+
+let builtins _lang env s =
+  match s with
+  | Type.Id { ns = Term ; name = Simple "abs_real" } ->
+    Type.builtin_term (Base.term_app1 (module Type) env s abs_real)
+  | _ -> `Not_found
+
+let typing_ext =
+  Dolmen_loop.Typer.Ext.create ~name:"abs_real_split" ~builtins
diff --git a/src/bin/dune b/src/bin/dune
index 3a5f51545..a9d87dc2d 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -1,4 +1,3 @@
-
 (executable
   (name           main)
   (public_name    dolmen)
@@ -6,9 +5,12 @@
   (libraries
     ; external deps
     cmdliner fmt gen
+    ; extension support
+    dune-site dune-site.plugins
     ; dolmen deps
     dolmen dolmen.intf dolmen.std
     dolmen_type dolmen_loop dolmen_model
+    dolmen_loop.bvconv dolmen_model.bvconv
     ; Memtrace dependency
     (select memory_profiler.ml from
             (memtrace -> memory_profiler.memtrace.ml)
@@ -28,3 +30,7 @@
  (files    dolmen.1)
  (package  dolmen_bin)
 )
+
+(generate_sites_module
+  (module Sites)
+  (plugins (dolmen plugins)))
diff --git a/src/bin/main.ml b/src/bin/main.ml
index cb2ee8070..0dce9df18 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -118,6 +118,13 @@ let doc conf t =
     pp_status t
     (Report.T.doc t)
 
+(* Extensions list *)
+(* *************** *)
+
+let list_extensions () =
+  let all = Options.list_extensions () in
+  Format.printf "%a@." Fmt.(vbox @@ list (box Options.pp_plugin)) all
+
 
 (* Main code *)
 (* ********* *)
@@ -146,3 +153,5 @@ let () =
     doc conf report
   | Ok (`Ok List_reports { conf; }) ->
     list conf
+  | Ok (`Ok List_extensions) ->
+    list_extensions ()
diff --git a/src/bin/options.ml b/src/bin/options.ml
index 53ab6d474..4e880825e 100644
--- a/src/bin/options.ml
+++ b/src/bin/options.ml
@@ -46,6 +46,7 @@ type cmd =
       report : Dolmen_loop.Report.T.t;
       conf : Dolmen_loop.Report.Conf.t;
     }
+  | List_extensions
 
 (* Color options *)
 (* ************************************************************************* *)
@@ -268,16 +269,195 @@ let report_style =
   ]
 
 
-(* Typing extensions *)
+(* Extensions *)
 (* ************************************************************************ *)
 
-let typing_extension_list =
-  List.map
-    (fun ext -> Loop.Typer.Ext.name ext, ext)
-    (Loop.Typer.Ext.list ())
+type extension_info = {
+  extension_name : string ;
+  (** Name of the extension (without dot). *)
+  typing_plugin : string option ;
+  (** Name of the Dune plugin that provide typing extensions. *)
+  model_plugin : string option ;
+  (** Name of the Dune plugin that provide model extensions. *)
+}
+
+let parse_ext_opt s =
+  match String.rindex s '.' with
+  | exception Not_found -> Some (s, None)
+  | pos ->
+    let extension_name = String.sub s 0 pos in
+    let plugin_kind = String.sub s (pos + 1) (String.length s - pos - 1) in
+    match plugin_kind with
+    | "typing" -> Some (extension_name, Some `Typing)
+    | "model" -> Some (extension_name, Some `Model)
+    | _ -> None
+
+let parse_plugin_opt s =
+  match String.rindex s '.' with
+  | exception Not_found ->
+    Some
+      { extension_name = s
+      ; typing_plugin = Some s
+      ; model_plugin = Some s }
+  | pos ->
+    let extension_name = String.sub s 0 pos in
+    let plugin_kind = String.sub s (pos + 1) (String.length s - pos - 1) in
+    match plugin_kind with
+    | "typing" ->
+      Some
+        { extension_name
+        ; typing_plugin = Some s
+        ; model_plugin = None }
+    | "model" ->
+      Some
+        { extension_name
+        ; typing_plugin = None
+        ; model_plugin = Some s }
+    | _ ->
+      (* Ignore plugins that do not conform to naming conventions *)
+      None
+
+let list_extensions () =
+  let tbl = Hashtbl.create 17 in
+  let err = ref [] in
+  let merge_plugins p1 p2 =
+    assert (p1.extension_name = p2.extension_name);
+    let typing_plugin =
+      match p1.typing_plugin, p2.typing_plugin with
+      | Some e, _ | _, Some e -> Some e
+      | None, None -> None
+    and model_plugin =
+      match p1.model_plugin, p2.model_plugin with
+      | Some e, _ | _, Some e -> Some e
+      | None, None -> None
+    in
+    { extension_name = p1.extension_name
+    ; typing_plugin
+    ; model_plugin }
+  in
+  let add_plugin n = function
+    | None -> err := (n, None) :: !err
+    | Some p ->
+      match Hashtbl.find tbl p.extension_name with
+      | p' -> Hashtbl.replace tbl p.extension_name (merge_plugins p p')
+      | exception Not_found -> Hashtbl.replace tbl p.extension_name p
+  in
+  List.iter (fun e ->
+    add_plugin e @@ parse_plugin_opt e
+  ) (Sites.Plugins.Plugins.list ());
+  let all = Hashtbl.fold (fun n p all -> (n, Some p) :: all) tbl !err in
+  List.fast_sort (fun (n1, _) (n2, _) -> String.compare n1 n2) all
+
+let pp_plugin ppf (n, p) =
+  match p with
+  | None ->
+    Fmt.pf ppf "%s@ %a" n
+      (Fmt.styled `Bold @@ Fmt.styled (`Fg (`Hi `Magenta)) @@ Fmt.string)
+        "IGNORED"
+  | Some p ->
+    let has_typing = Option.is_some p.typing_plugin in
+    let has_model = Option.is_some p.model_plugin in
+    let variants =
+      (if has_typing then ["typing"] else []) @
+      (if has_model then ["model"] else [])
+    in
+    Fmt.pf ppf "%s@ %a" p.extension_name
+      Fmt.(parens @@ list ~sep:comma string) variants
 
-let typing_ext =
-  Arg.enum typing_extension_list
+let pp_kind ppf = function
+  | `Typing -> Fmt.pf ppf "typing"
+  | `Model -> Fmt.pf ppf "model"
+
+(* Find the plugin implementing extension kind [kind] for extension [name],
+   e.g. ["bvconv.typing"] for [name = "bvconv"] and [kind = `Typing]. *)
+let find_ext name kind =
+  try
+    Ok (
+      List.find (fun pname ->
+        match parse_ext_opt pname with
+        | None -> false
+        | Some (name', kind') ->
+          if String.equal name name' then
+            match kind' with
+            | Some k' when k' = kind -> true
+            | None -> true
+            | _ -> false
+          else
+            false
+      ) (Sites.Plugins.Plugins.list ())
+    )
+  with Not_found ->
+    Fmt.error_msg
+      "@[<v>Could not find %a extension '%s'@ \
+      Available extensions:@;<1 2>@[<v>%a@]@]"
+      pp_kind kind name
+      Fmt.(list (box pp_plugin)) (list_extensions ())
+
+type _ extension_kind =
+  | Typing : Dolmen_loop.Typer.Ext.t extension_kind
+  | Model : Dolmen_model.Env.Ext.t extension_kind
+
+let erase_kind (type a) : a extension_kind -> _ = function
+  | Typing -> `Typing
+  | Model -> `Model
+
+let find_and_load_ext (type a) : string -> a extension_kind -> (a, _) result =
+  fun name kind ->
+    match find_ext name (erase_kind kind) with
+    | Error _ as e -> e
+    | Ok plugin ->
+      Sites.Plugins.Plugins.load plugin;
+      match kind with
+      | Typing -> (
+          try
+            Ok (List.find
+              (fun e -> Dolmen_loop.Typer.Ext.name e = name)
+              (Dolmen_loop.Typer.Ext.list ())
+            )
+          with Not_found ->
+            Fmt.error_msg
+              "Plugin '%s' did not register a typing extension for '%s'"
+              plugin name
+      )
+      | Model -> (
+          try
+            Ok (List.find
+              (fun e -> Dolmen_model.Env.Ext.name e = name)
+              (Dolmen_model.Env.Ext.list ())
+            )
+          with Not_found ->
+            Fmt.error_msg
+              "Plugin '%s' did not register a model extension for '%s'"
+              plugin name
+      )
+
+type extension =
+  { typing_extension :
+      (Dolmen_loop.Typer.Ext.t option, [ `Msg of string ]) result
+  ; model_extension :
+      (Dolmen_model.Env.Ext.t option, [ `Msg of string ]) result
+  }
+
+let extension =
+  let parse s =
+    match parse_ext_opt s with
+    | None -> Fmt.error_msg "Invalid extension name '%s'" s
+    | Some (name, kind) ->
+      let typing_extension =
+        match kind with
+        | None | Some `Typing ->
+          Result.map Option.some (find_and_load_ext name Typing)
+        | _ -> Ok None
+      and model_extension =
+        match kind with
+        | None | Some `Model ->
+          Result.map Option.some (find_and_load_ext name Model)
+        | _ -> Ok None
+      in
+      Ok { typing_extension ; model_extension }
+  in
+  let print ppf _p = Fmt.pf ppf "" in
+  Arg.conv (parse, print)
 
 
 (* Smtlib2 logic and extensions *)
@@ -366,7 +546,7 @@ let mk_run_state
     flow_check
     header_check header_licenses header_lang_version
     smtlib2_forced_logic smtlib2_exts
-    type_check extension_builtins
+    type_check extensions
     check_model (* check_model_mode *)
     debug report_style max_warn reports syntax_error_ref
   =
@@ -383,27 +563,55 @@ let mk_run_state
   let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in
   let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in
   let () = Hints.model ~check_model (* ~check_model_mode *) in
+  (* Extensions *)
+  let typing_exts =
+    List.fold_left (fun typing_exts p ->
+      Result.bind typing_exts @@ fun typing_exts ->
+      match p.typing_extension with
+      | Ok None -> Ok typing_exts
+      | Ok (Some ext) ->
+        Ok (ext :: typing_exts)
+      | Error _ as e -> e
+    ) (Ok []) extensions
+  in
+  Result.bind typing_exts @@ fun typing_extension_builtins ->
+  let model_exts =
+    if check_model then
+      List.fold_left (fun model_exts p ->
+        Result.bind model_exts @@ fun model_exts ->
+        match p.model_extension with
+        | Ok None -> Ok model_exts
+        | Ok (Some ext) ->
+          Ok (ext :: model_exts)
+        | Error _ as e -> e
+      ) (Ok []) extensions
+    else
+      Ok []
+  in
+  Result.bind model_exts @@ fun model_extension_builtins ->
   (* State creation *)
-  Loop.State.empty
-  |> Loop.State.init
-    ~bt ~debug ~report_style ~reports
-    ~max_warn ~time_limit ~size_limit
-    ~response_file
-  |> Loop.Parser.init
-    ~syntax_error_ref
-    ~interactive_prompt:Loop.Parser.interactive_prompt_lang
-  |> Loop.Typer.init
-    ~smtlib2_forced_logic
-    ~extension_builtins
-  |> Loop.Typer_Pipe.init ~type_check
-  |> Loop.Check.init
-    ~check_model
-    (* ~check_model_mode *)
-  |> Loop.Flow.init ~flow_check
-  |> Loop.Header.init
-    ~header_check
-    ~header_licenses
-    ~header_lang_version
+  Ok (
+    Loop.State.empty
+    |> Loop.State.init
+      ~bt ~debug ~report_style ~reports
+      ~max_warn ~time_limit ~size_limit
+      ~response_file
+    |> Loop.Parser.init
+      ~syntax_error_ref
+      ~interactive_prompt:Loop.Parser.interactive_prompt_lang
+    |> Loop.Typer.init
+      ~smtlib2_forced_logic
+      ~extension_builtins:typing_extension_builtins
+    |> Loop.Typer_Pipe.init ~type_check
+    |> Loop.Check.init
+      ~check_model ~extension_builtins:model_extension_builtins
+      (* ~check_model_mode *)
+    |> Loop.Flow.init ~flow_check
+    |> Loop.Header.init
+      ~header_check
+      ~header_licenses
+      ~header_lang_version
+  )
 
 (* Profiling *)
 (* ************************************************************************* *)
@@ -627,12 +835,12 @@ let state =
     Arg.(value & opt_all smtlib2_ext [] &
          info ["internal-smtlib2-extension"] ~docs:internal_section ~doc)
   in
-  let typing_ext =
+  let ext =
     let doc = Format.asprintf
-        "Enable typing extensions.
-         $(docv) must be %s" (Arg.doc_alts_enum typing_extension_list)
+        "Enable extensions. Use $(b,--list-extensions) to list available \
+        extensions."
     in
-    Arg.(value & opt_all typing_ext [] &
+    Arg.(value & opt_all extension [] &
          info ["ext"] ~docs ~doc)
   in
   let debug =
@@ -689,7 +897,8 @@ let state =
       in
       Arg.(value & opt bool false & info ["syntax-error-ref"] ~doc ~docs:error_section)
     in
-  Term.(const mk_run_state $ profiling_t $
+  Term.(term_result (
+    const mk_run_state $ profiling_t $
         gc $ gc_t $ bt $ colors $
         abort_on_bug $
         time $ size $
@@ -697,9 +906,9 @@ let state =
         flow_check $
         header_check $ header_licenses $ header_lang_version $
         force_smtlib2_logic $ smtlib2_extensions $
-        typing $ typing_ext $
+        typing $ ext $
         check_model $ (* check_model_mode $ *)
-        debug $ report_style $ max_warn $ reports $ syntax_error_ref)
+        debug $ report_style $ max_warn $ reports $ syntax_error_ref))
 
 
 (* List command term *)
@@ -707,19 +916,21 @@ let state =
 
 let cli =
   let docs = option_section in
-  let aux state preludes logic_file list doc =
-    match list, doc with
-    | false, None ->
+  let aux state preludes logic_file list doc list_extensions =
+    match list, doc, list_extensions with
+    | false, None, false ->
       `Ok (Run { state; logic_file; preludes })
-    | false, Some report ->
+    | false, Some report, false ->
       let conf = Loop.State.get Loop.State.reports state in
       `Ok (Doc { report; conf; })
-    | true, None ->
+    | true, None, false ->
       let conf = Loop.State.get Loop.State.reports state in
       `Ok (List_reports { conf; })
-    | true, Some _ ->
+    | false, None, true ->
+      `Ok List_extensions
+    | _ ->
       `Error (false,
-              "at most one of --list and --doc might be \
+              "at most one of --list, --doc and --list-extensions might be \
                present on the command line")
   in
   let list =
@@ -731,4 +942,11 @@ let cli =
     let doc = "The warning or error of which to show the documentation." in
     Arg.(value & opt (some mnemonic_conv) None & info ["doc"] ~doc ~docv:"mnemonic" ~docs)
   in
-  Term.(ret (const aux $ state $ preludes $ logic_file $ list $ doc))
+  let list_extensions =
+    let doc = "List all available extensions." in
+    Arg.(value & flag & info ["list-extensions"] ~doc ~docs)
+  in
+  Term.(ret (
+    const aux $ state $ preludes $ logic_file $ list $ doc
+    $ list_extensions
+  ))
diff --git a/src/loop/extensions/bvconv.ml b/src/loop/extensions/bvconv.ml
new file mode 100644
index 000000000..7bdce70f1
--- /dev/null
+++ b/src/loop/extensions/bvconv.ml
@@ -0,0 +1,10 @@
+module Smtlib2_Bvconv =
+  Dolmen_type.Bitv.Smtlib2.Bvconv(Dolmen_loop.Typer.T)
+    (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
+
+let typing_extension =
+  Dolmen_loop.Typer.Ext.create ~name:"bvconv"
+    ~builtins:(function
+      | `Logic Dolmen_loop.Logic.Smtlib2 version ->
+        Smtlib2_Bvconv.parse (`Script version)
+      | _ -> Dolmen_type.Base.noop)
diff --git a/src/loop/extensions/dune b/src/loop/extensions/dune
new file mode 100644
index 000000000..254e2d7e0
--- /dev/null
+++ b/src/loop/extensions/dune
@@ -0,0 +1,11 @@
+(library
+  (public_name dolmen_loop.bvconv)
+  (name bvconv_typing)
+  (modules bvconv)
+  (libraries dolmen_type dolmen_loop))
+
+(plugin
+  (name bvconv.typing)
+  (package dolmen_loop)
+  (libraries dolmen_loop.bvconv)
+  (site (dolmen plugins)))
diff --git a/src/loop/typer.ml b/src/loop/typer.ml
index e14e44e44..384fb5ead 100644
--- a/src/loop/typer.ml
+++ b/src/loop/typer.ml
@@ -55,9 +55,6 @@ module Smtlib2_Arrays =
 module Smtlib2_Bitv =
   Dolmen_type.Bitv.Smtlib2.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
-module Smtlib2_Bvconv =
-  Dolmen_type.Bitv.Smtlib2.Bvconv(T)
-    (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
 module Smtlib2_Float =
   Dolmen_type.Float.Smtlib2.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
@@ -73,6 +70,28 @@ module Zf_arith =
   Dolmen_type.Arith.Zf.Thf(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
 
+(* Extensions builtins *)
+(* ************************************************************************ *)
+
+module Ext = struct
+
+  type t = {
+    name : string;
+    builtins : Typer_intf.lang -> T.builtin_symbols;
+  }
+
+  let all = ref []
+  let list () = !all
+  let name { name; _ } = name
+  let builtins { builtins; _ } = builtins
+
+  let create ~name ~builtins =
+    let t = { name; builtins; } in
+    all := t :: !all;
+    t
+end
+
+
 (* Printing helpers *)
 (* ************************************************************************ *)
 
@@ -1075,40 +1094,7 @@ module Typer(State : State.S) = struct
   type error = T.error
   type warning = T.warning
   type builtin_symbols = T.builtin_symbols
-
-  type lang = [
-    | `Logic of Logic.language
-    | `Response of Response.language
-  ]
-
-  (* Extensions builtins *)
-  (* ************************************************************************ *)
-
-  module Ext = struct
-
-    type t = {
-      name : string;
-      builtins : lang -> T.builtin_symbols;
-    }
-
-    let all = ref []
-    let list () = !all
-    let name { name; _ } = name
-    let builtins { builtins; _ } = builtins
-
-    let create ~name ~builtins =
-      let t = { name; builtins; } in
-      all := t :: !all;
-      t
-
-    let bv2nat =
-      create ~name:"bvconv"
-        ~builtins:(function
-            | `Logic Logic.Smtlib2 version ->
-              Smtlib2_Bvconv.parse (`Script version)
-            | _ -> Dolmen_type.Base.noop)
-
-  end
+  type extension = Ext.t
 
   (* State setup *)
   (* ************************************************************************ *)
@@ -1122,7 +1108,8 @@ module Typer(State : State.S) = struct
     State.create_key ~pipe "smtlib2_forced_logic"
   let extension_builtins : Ext.t list State.key =
     State.create_key ~pipe "extensions_builtins"
-  let additional_builtins : (state -> lang -> T.builtin_symbols) State.key =
+  let additional_builtins :
+    (state -> Typer_intf.lang -> T.builtin_symbols) State.key =
     State.create_key ~pipe "additional_builtins"
 
   let init
@@ -1161,7 +1148,7 @@ module Typer(State : State.S) = struct
     | `Logic f -> f.loc
     | `Response f -> f.loc
 
-  let lang_of_input (input : input) : [ lang | `Missing ]=
+  let lang_of_input (input : input) : [ Typer_intf.lang | `Missing ] =
     match input with
     | `Logic f ->
       begin match f.lang with
@@ -1484,7 +1471,7 @@ module Typer(State : State.S) = struct
     (* Match the language to determine bultins and other options *)
     let lang =
       match lang_of_input input with
-      | #lang as lang -> lang
+      | #Typer_intf.lang as lang -> lang
       | `Missing ->
         let st =
           error st ~input ~loc:{ file; loc; } Report.Error.internal_error
diff --git a/src/loop/typer.mli b/src/loop/typer.mli
index aaf061eca..f3dd23023 100644
--- a/src/loop/typer.mli
+++ b/src/loop/typer.mli
@@ -40,6 +40,30 @@ val bad_arith_expr : (Dolmen_type.Arith.Smtlib2.config * string) Report.Warning.
 val unknown_logic : string Report.Warning.t
 (** Unknown logic warning *)
 
+module Ext : sig
+  (** Define typing extensions.
+
+      These extensions are typically extensions used by some community,
+      but not yet part of the standard.
+
+      @since 0.10 *)
+
+  type t
+  (** The type of typing extensions. *)
+
+  val name : t -> string
+  (** Extension name, sould be suitable for cli options. *)
+
+  val builtins : t -> Typer_intf.lang -> T.builtin_symbols
+  (** Reutnrs the typing builtins from an extension. *)
+
+  val create :
+    name:string -> builtins:(Typer_intf.lang -> T.builtin_symbols) -> t
+  (** Create a new extension. *)
+
+  val list : unit -> t list
+  (** The list of all extensions. *)
+end
 
 (** {2 Typechecker Functor} *)
 
@@ -54,6 +78,7 @@ module Typer(State : State.S)
                 and type error = T.error
                 and type warning = T.warning
                 and type builtin_symbols = T.builtin_symbols
+                and type extension = Ext.t
 
 (** {2 Typechecker Pipe} *)
 
diff --git a/src/loop/typer_intf.ml b/src/loop/typer_intf.ml
index 31074060f..5ac3c2979 100644
--- a/src/loop/typer_intf.ml
+++ b/src/loop/typer_intf.ml
@@ -1,4 +1,9 @@
-(* This file is free software, part of Archsat. See file "LICENSE" for more details. *)
+(* This file is free software, part of dolmen. See file "LICENSE" for more details. *)
+
+type lang = [
+  | `Logic of Logic.language
+  | `Response of Response.language
+]
 
 (* Small signature to define a number of types. *)
 module type Types = sig
@@ -31,11 +36,6 @@ module type Typer = sig
     | `Response of Response.language State.file
   ]
 
-  type lang = [
-    | `Logic of Logic.language
-    | `Response of Response.language
-  ]
-
   type decl = [
     | `Type_decl of ty_cst * ty_def option
     | `Term_decl of term_cst
@@ -129,6 +129,9 @@ module type Typer_Full = sig
   type builtin_symbols
   (** The type of builin symbols for the type-checker. *)
 
+  type extension
+  (** The type of extensions for the type-checker. *)
+
   include Typer
     with type env := env
      and type state := state
@@ -143,34 +146,6 @@ module type Typer_Full = sig
   (** This signature includes the requirements to instantiate the {Pipes.Make:
       functor*)
 
-  module Ext : sig
-    (** Define typing extensions.
-
-        These extensions are typically extensions used by some community,
-        but not yet part of the standard.
-
-        @since 0.10 *)
-
-    type t
-    (** The type of typing extensions. *)
-
-    val name : t -> string
-    (** Extension name, sould be suitable for cli options. *)
-
-    val builtins : t -> lang -> builtin_symbols
-    (** Reutnrs the typing builtins from an extension. *)
-
-    val create : name:string -> builtins:(lang -> builtin_symbols) -> t
-    (** Create a new extension. *)
-
-    val list : unit -> t list
-    (** The list of all extensions. *)
-
-    val bv2nat : t
-    (** Typing extension to add the `bv2nat` function. *)
-
-  end
-
   val ty_state : ty_state key
   (** Key to store the local typechecking state in the global pipeline state. *)
 
@@ -181,7 +156,7 @@ module type Typer_Full = sig
   (** Force the typechecker to use the given logic (instead of using the one declared
       in the `set-logic` statement). *)
 
-  val extension_builtins : Ext.t list key
+  val extension_builtins : extension list key
   (** Use typing extensions defined by the typechecker.
 
       @since 0.10 *)
@@ -197,7 +172,7 @@ module type Typer_Full = sig
   val init :
     ?ty_state:ty_state ->
     ?smtlib2_forced_logic:string option ->
-    ?extension_builtins:(Ext.t list) ->
+    ?extension_builtins:(extension list) ->
     ?additional_builtins:(state -> lang -> builtin_symbols) ->
     state -> state
 
diff --git a/src/model/bitv.ml b/src/model/bitv.ml
index 7ea4ca820..68b513b90 100644
--- a/src/model/bitv.ml
+++ b/src/model/bitv.ml
@@ -29,8 +29,6 @@ let ops = Value.ops ~print ~compare ()
 (* Value helpers *)
 (* ************************************************************************* *)
 
-
-
 let is_unsigned_integer size z =
   Z.sign z >= 0 && Z.numbits z <= size
 
@@ -198,4 +196,3 @@ let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Bitv_sgt n -> cmp ~cst (fun a b -> Z.gt (sbitv n a) (sbitv n b))
   | B.Bitv_sge n -> cmp ~cst (fun a b -> Z.geq (sbitv n a) (sbitv n b))
   | _ -> None
-
diff --git a/src/model/env.ml b/src/model/env.ml
index ebf308351..4fb13fcc9 100644
--- a/src/model/env.ml
+++ b/src/model/env.ml
@@ -28,4 +28,22 @@ let model { model; _ } = model
 
 let update_model t f = { t with model = f t.model; }
 
-
+(* Extensions builtins *)
+(* ************************************************************************ *)
+
+module Ext = struct
+  type t = {
+    name : string;
+    builtins : builtins;
+  }
+
+  let all = ref []
+  let list () = !all
+  let name { name; _ } = name
+  let builtins { builtins; _ } = builtins
+
+  let create ~name ~builtins =
+    let t = { name; builtins; } in
+    all := t :: !all;
+    t
+end
diff --git a/src/model/env.mli b/src/model/env.mli
index ed9ef6d38..a76082a67 100644
--- a/src/model/env.mli
+++ b/src/model/env.mli
@@ -21,4 +21,20 @@ val model : t -> Model.t
 
 val update_model : t -> (Model.t -> Model.t) -> t
 
+module Ext : sig
+  type t
+  (** The type of evaluation extensions. *)
 
+  val name : t -> string
+  (** Extension name, should be suitable for cli options. *)
+
+  val builtins : t -> builtins
+  (** Returns the evaluation builtins from an extension. *)
+
+  val create :
+    name:string -> builtins:builtins -> t
+  (** Create a new extension. *)
+
+  val list : unit -> t list
+  (** The list of all extensions. *)
+end
diff --git a/src/model/extensions/bvconv.ml b/src/model/extensions/bvconv.ml
new file mode 100644
index 000000000..268d968be
--- /dev/null
+++ b/src/model/extensions/bvconv.ml
@@ -0,0 +1,22 @@
+module B = Dolmen.Std.Builtin
+module Fun = Dolmen_model.Fun
+
+let int = Dolmen_model.Int.mk
+let of_int = Dolmen_model.Value.extract_exn ~ops:Dolmen_model.Int.ops
+let bitv ~size x = Dolmen_model.Bitv.mk size (Z.extract x 0 size)
+let of_bitv ~size = Dolmen_model.Bitv.ubitv size
+
+let bv2nat ~cst ~size =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> int (of_bitv ~size x)))
+
+let int2bv ~cst ~size =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> bitv ~size (of_int x)))
+
+let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | B.Bitv_of_int { n } -> int2bv ~cst ~size:n
+  | B.Bitv_to_nat { n } -> bv2nat ~cst ~size:n
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Env.Ext.create ~name:"bvconv" ~builtins
diff --git a/src/model/extensions/dune b/src/model/extensions/dune
new file mode 100644
index 000000000..8a149aca9
--- /dev/null
+++ b/src/model/extensions/dune
@@ -0,0 +1,11 @@
+(library
+  (public_name dolmen_model.bvconv)
+  (name bvconv_model)
+  (modules bvconv)
+  (libraries dolmen dolmen_model))
+
+(plugin
+  (name bvconv.model)
+  (package dolmen_model)
+  (libraries dolmen_model.bvconv)
+  (site (dolmen plugins)))
diff --git a/src/model/loop.ml b/src/model/loop.ml
index 384905936..4df070d4a 100644
--- a/src/model/loop.ml
+++ b/src/model/loop.ml
@@ -265,40 +265,45 @@ module Make
       and type formula := Dolmen.Std.Expr.formula)
 = struct
 
+  let core_builtins =
+    Eval.builtins [
+      Adt.builtins;
+      Bool.builtins;
+      Core.builtins;
+      Array.builtins;
+      Int.builtins;
+      Rat.builtins;
+      Real.builtins;
+      Bitv.builtins;
+      Fp.builtins;
+      Coercion.builtins;
+    ]
+
   let pipe = "Model"
   let check_model = Typer.check_model
   let check_state = State.create_key ~pipe "check_state"
+  let builtins = State.create_key ~pipe "builtins"
 
   let init
       ~check_model:check_model_value
+      ?(extension_builtins=[])
       st =
+    let extension_builtins = List.map Env.Ext.builtins extension_builtins in
     st
     |> State.set check_model check_model_value
     |> State.set check_state empty
+    |> State.set builtins
+      (Eval.builtins (core_builtins :: extension_builtins))
 
 
   (* Evaluation and errors *)
   (* ************************************************************************ *)
 
-  let builtins =
-    Eval.builtins [
-      Adt.builtins;
-      Bool.builtins;
-      Core.builtins;
-      Array.builtins;
-      Int.builtins;
-      Rat.builtins;
-      Real.builtins;
-      Bitv.builtins;
-      Fp.builtins;
-      Coercion.builtins;
-    ]
-
   let eval ~reraise_for_delayed_eval ~file ~loc st model term =
     let _err err args =
       raise (State.Error (State.error st ~file ~loc err args))
     in
-    let env = Env.mk model ~builtins in
+    let env = Env.mk model ~builtins:(State.get builtins st) in
     try
       Eval.eval env term
     with