diff --git a/caisar.opam b/caisar.opam
index 6f7f353f296c2da62f478dc0791eaaa5e7e6dca1..7c53587d0a4b8c74f437369542ba38338abb219c 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -5,6 +5,8 @@ synopsis: "Framework for neural network verification"
 depends: [
   "ocaml" {>= "4.10"}
   "dune" {>= "2.9" & >= "2.9.0"}
+  "dune-site" {>= "2.9.0"}
+  "why3"
   "base" {>= "v0.14.0"}
   "cmdliner" {>= "1.0.4"}
   "fmt" {>= "0.8.9"}
diff --git a/config/dune b/config/dune
new file mode 100644
index 0000000000000000000000000000000000000000..1aabdf75ad87b38d9be62f9e82b4d5859a2f7a81
--- /dev/null
+++ b/config/dune
@@ -0,0 +1,4 @@
+(install
+ (section (site (caisar config)))
+ (files provers_autodetection.conf)
+(package caisar))
diff --git a/config/provers_autodetection.conf b/config/provers_autodetection.conf
new file mode 100644
index 0000000000000000000000000000000000000000..688a4de8d0f5a2828ffbf46e6ade2ce05f74269b
--- /dev/null
+++ b/config/provers_autodetection.conf
@@ -0,0 +1,12 @@
+[ATP alt-ergo]
+name = "Alt-Ergo"
+exec = "alt-ergo"
+exec = "alt-ergo-2.4.0"
+version_switch = "--version"
+version_regexp = "^\\([0-9.]+\\)$"
+version_ok  = "2.4.0"
+command = "%e --timelimit %t %f"
+command_steps = "%e --steps-bound %S %f"
+driver = "alt_ergo"
+editor = "altgr-ergo"
+use_at_auto_level = 1
diff --git a/dune-project b/dune-project
index e4049ba8dbe74d07176a7f74eb858fa9f0765888..610e405cc8bb2069908819f343798e4d909bb84b 100644
--- a/dune-project
+++ b/dune-project
@@ -15,6 +15,8 @@
   (depends
    (ocaml (>= 4.10))
    (dune (>= 2.9.0))
+   (dune-site (>= 2.9.0))
+   why3
    (base (>= v0.14.0))
    (cmdliner (>= 1.0.4))
    (fmt (>= 0.8.9))
@@ -25,7 +27,7 @@
    (ppx_deriving_yojson (>= 3.6.1))
    (csv (>= 2.4))
   )
-  (sites (lib stdlib))
+  (sites (share stdlib)(share config))
 )
 
 (package
diff --git a/src/detection.ml b/src/detection.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ed15cdc15bf5bf686309eab4e8993a7c785833b2
--- /dev/null
+++ b/src/detection.ml
@@ -0,0 +1,24 @@
+open Base
+module Sys = Caml.Sys
+
+let null = if Sys.unix then "/dev/null" else "NUL"
+
+let rec lookup_file l f =
+  match l with
+  | [] -> raise Caml.Not_found
+  | a :: l ->
+      let abs = Caml.Filename.concat a f in
+      if Sys.file_exists abs then abs else lookup_file l f
+
+let detect () =
+  Why3.Debug.set_flag Why3.Autodetection.debug;
+  let caisar_autodetection =
+    lookup_file Stdlib_path.Sites.config "provers_autodetection.conf"
+  in
+  let data =
+    Why3.Autodetection.Prover_autodetection_data.from_file caisar_autodetection
+  in
+  let config = Why3.Whyconf.init_config (Some null) in
+  let binaries = Why3.Autodetection.request_binaries_version config data in
+  let provers = Why3.Autodetection.compute_builtin_prover binaries data in
+  Why3.Whyconf.set_provers config provers
diff --git a/src/prove.ml b/src/prove.ml
index cc59ea6c76518c55317f9beaf21bc39d21abd80a..bdddcae4af7b0851250da637f8aa8a207cf84d7c 100644
--- a/src/prove.ml
+++ b/src/prove.ml
@@ -3,13 +3,16 @@ open Base
 let () = Language.register ()
 
 let create_env loadpath =
+  let conf = Detection.detect () in
   let stdlib = Stdlib_path.Sites.stdlib in
-  let conf = Why3.Whyconf.init_config None in
-  Why3.Env.create_env
-    (loadpath @ stdlib @ Why3.Whyconf.loadpath (Why3.Whyconf.get_main conf))
+  ( Why3.Env.create_env
+      (loadpath @ stdlib @ Why3.Whyconf.loadpath (Why3.Whyconf.get_main conf)),
+    conf )
+
+let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
 
 let prove format loadpath file =
-  let env = create_env loadpath in
+  let env, config = create_env loadpath in
   let _, m =
     match file with
     | "-" ->
@@ -25,5 +28,9 @@ let prove format loadpath file =
   Why3.Wstdlib.Mstr.iter
     (fun _ th ->
       let l = Why3.Task.split_theory th None None in
-      List.iter l ~f:(Fmt.pr "%a" Why3.Pretty.print_task))
+      let prover = Why3.Whyconf.filter_one_prover config altergo in
+      let driver =
+        Why3.Whyconf.load_driver (Why3.Whyconf.get_main config) env prover
+      in
+      List.iter l ~f:(Fmt.pr "%a" (Why3.Driver.print_task driver)))
     m