diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
new file mode 100644
index 0000000..38e133c
--- /dev/null
+++ b/.github/workflows/build.yml
@@ -0,0 +1,35 @@
+name: Build
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - self-hosted
+        ocaml-compiler:
+          - "4.14"
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+      - name: Setup OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+      - name: Install dependencies
+        run: opam install -y . --deps-only --with-test
+      - name: Build
+        run: opam exec -- dune build @install
+      - name: Test
+        run: opam exec -- dune runtest
diff --git a/.ocamlformat b/.ocamlformat
new file mode 100644
index 0000000..5c3c54e
--- /dev/null
+++ b/.ocamlformat
@@ -0,0 +1,43 @@
+version=0.26.1
+assignment-operator=end-line
+break-cases=fit
+break-fun-decl=wrap
+break-fun-sig=wrap
+break-infix=wrap
+break-infix-before-func=false
+break-separators=before
+break-sequences=true
+cases-exp-indent=2
+cases-matching-exp-indent=normal
+doc-comments=before
+doc-comments-padding=2
+doc-comments-tag-only=default
+dock-collection-brackets=false
+exp-grouping=preserve
+field-space=loose
+if-then-else=compact
+indicate-multiline-delimiters=space
+indicate-nested-or-patterns=unsafe-no
+infix-precedence=indent
+leading-nested-match-parens=false
+let-and=sparse
+let-binding-spacing=compact
+let-module=compact
+margin=80
+max-indent=2
+module-item-spacing=sparse
+ocaml-version=4.14.0
+ocp-indent-compat=false
+parens-ite=false
+parens-tuple=always
+parse-docstrings=true
+sequence-blank-line=preserve-one
+sequence-style=terminator
+single-case=compact
+space-around-arrays=true
+space-around-lists=true
+space-around-records=true
+space-around-variants=true
+type-decl=sparse
+wrap-comments=false
+wrap-fun-args=true
\ No newline at end of file
diff --git a/api/build_enums.ml b/api/build_enums.ml
index f5ae294..8b00e65 100644
--- a/api/build_enums.ml
+++ b/api/build_enums.ml
@@ -1 +1 @@
-external build_enums : unit -> unit = "build_enums"
\ No newline at end of file
+external build_enums : unit -> unit = "build_enums"
diff --git a/api/cvc5_enums.ml b/api/cvc5_enums.ml
index 0db1139..604deb1 100644
--- a/api/cvc5_enums.ml
+++ b/api/cvc5_enums.ml
@@ -1,4 +1,3 @@
 open Build_enums
 
-let () =
-  build_enums ()
\ No newline at end of file
+let () = build_enums ()
diff --git a/api/dune b/api/dune
index ccf8d43..6cad891 100644
--- a/api/dune
+++ b/api/dune
@@ -6,15 +6,12 @@
 (library
  (name build_enums)
  (modules build_enums)
+ (no_dynlink)
  (foreign_stubs
   (language cxx)
   (names build_enums)
+  (extra_deps ../cvc5_export.h)
   (flags :standard -std=c++17 -I/opt/homebrew/include)
-  (include_dirs 
-   ../vendor/cvc5/include))
- (foreign_archives
-  ../vendor/cvc5
-  ../vendor/cadical
-  ../vendor/picpoly
-  ../vendor/picpolyxx)
- (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp))
\ No newline at end of file
+  (include_dirs ../vendor/cvc5/include))
+ (foreign_archives ../cvc5 ../cadical ../picpoly ../picpolyxx)
+ (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp))
diff --git a/cvc5.ml b/cvc5.ml
index 99595b4..89f2289 100644
--- a/cvc5.ml
+++ b/cvc5.ml
@@ -5,67 +5,88 @@ let _ = Callback.register_exception "cvc5Exception" (Error "")
 module Kind = Cvc5_enums.Kind
 module RoundingMode = Cvc5_enums.RoundingMode
 
-module TermManager =
-struct
+module TermManager = struct
   type tm = Cvc5_external.term_manager
 
   let mk_tm = Cvc5_external.new_term_manager
+
   let delete_tm = Cvc5_external.delete_term_manager
 end
 
-module Sort =
-struct
+module Sort = struct
   type sort = Cvc5_external.sort
 
   let mk_bool_sort = Cvc5_external.get_boolean_sort
+
   let mk_int_sort = Cvc5_external.get_integer_sort
-  let mk_real_sort = Cvc5_external.get_real_sort 
-  let mk_string_sort = Cvc5_external.get_string_sort 
+
+  let mk_real_sort = Cvc5_external.get_real_sort
+
+  let mk_string_sort = Cvc5_external.get_string_sort
+
   let mk_bv_sort = Cvc5_external.mk_bitvector_sort
 end
 
-module Term =
-struct
+module Term = struct
   type term = Cvc5_external.term
 
   let id = Cvc5_external.term_id
+
   let equal = Cvc5_external.term_equal
+
   let kind t = Kind.of_cpp @@ Cvc5_external.term_kind t
+
   let sort = Cvc5_external.term_sort
+
   let to_string = Cvc5_external.term_to_string
+
   let mk_const = Cvc5_external.mk_const
+
   let mk_const_s = Cvc5_external.mk_const_s
+
   let mk_term (tm : TermManager.tm) (k : Kind.t) (terms : term array) =
     Cvc5_external.mk_term tm (Kind.to_cpp k) terms
+
   let mk_true = Cvc5_external.mk_true
+
   let mk_false = Cvc5_external.mk_false
+
   let mk_bool = Cvc5_external.mk_bool
+
   let mk_int = Cvc5_external.mk_int
-  let mk_rm (tm : TermManager.tm) (rm : RoundingMode.t) = 
+
+  let mk_rm (tm : TermManager.tm) (rm : RoundingMode.t) =
     Cvc5_external.mk_roundingmode tm (RoundingMode.to_cpp rm)
 end
 
-module Result =
-struct
+module Result = struct
   type result = Cvc5_external.result
 
   let is_sat = Cvc5_external.result_is_sat
+
   let is_unsat = Cvc5_external.result_is_unsat
+
   let is_unknown = Cvc5_external.result_is_unknown
 end
 
-module Solver =
-struct
+module Solver = struct
   type solver = Cvc5_external.solver
 
   let mk_solver = Cvc5_external.new_solver
+
   let delete_solver = Cvc5_external.delete
+
   let assert_formula = Cvc5_external.assert_formula
+
   let check_sat = Cvc5_external.check_sat
+
   let set_logic = Cvc5_external.set_logic
+
   let simplify = Cvc5_external.simplify
+
   let push = Cvc5_external.push
+
   let pop = Cvc5_external.pop
+
   let reset = Cvc5_external.reset_assertions
 end
-
diff --git a/cvc5.mli b/cvc5.mli
index 1192015..590c5c6 100644
--- a/cvc5.mli
+++ b/cvc5.mli
@@ -3,64 +3,86 @@ exception Error of string
 module Kind = Cvc5_enums.Kind
 module RoundingMode = Cvc5_enums.RoundingMode
 
-module TermManager :
-sig 
+module TermManager : sig
   type tm
 
   val mk_tm : unit -> tm
+
   val delete_tm : tm -> unit
 end
 
-module Sort : 
-sig
+module Sort : sig
   type sort
-  
+
   val mk_bool_sort : TermManager.tm -> sort
+
   val mk_int_sort : TermManager.tm -> sort
+
   val mk_real_sort : TermManager.tm -> sort
+
   val mk_string_sort : TermManager.tm -> sort
+
   val mk_bv_sort : TermManager.tm -> int -> sort
 end
 
-module Term : 
-sig 
+module Term : sig
   type term
 
   val id : term -> int
+
   val equal : term -> term -> bool
+
   val kind : term -> Kind.t
+
   val sort : term -> Sort.sort
+
   val to_string : term -> string
+
   val mk_const : TermManager.tm -> Sort.sort -> term
+
   val mk_const_s : TermManager.tm -> Sort.sort -> string -> term
+
   val mk_term : TermManager.tm -> Kind.t -> term array -> term
+
   val mk_true : TermManager.tm -> term
+
   val mk_false : TermManager.tm -> term
+
   val mk_bool : TermManager.tm -> bool -> term
+
   val mk_int : TermManager.tm -> int -> term
+
   val mk_rm : TermManager.tm -> RoundingMode.t -> term
 end
 
-module Result : 
-sig 
-  type result 
+module Result : sig
+  type result
 
   val is_sat : result -> bool
+
   val is_unsat : result -> bool
+
   val is_unknown : result -> bool
 end
 
-module Solver :
-sig
+module Solver : sig
   type solver
 
   val mk_solver : TermManager.tm -> solver
+
   val delete_solver : solver -> unit
+
   val assert_formula : solver -> Term.term -> unit
+
   val check_sat : solver -> Result.result
+
   val set_logic : solver -> string -> unit
+
   val simplify : solver -> Term.term -> Term.term
+
   val push : solver -> int -> unit
+
   val pop : solver -> int -> unit
+
   val reset : solver -> unit
-end
\ No newline at end of file
+end
diff --git a/cvc5.opam b/cvc5.opam
new file mode 100644
index 0000000..7b6b91b
--- /dev/null
+++ b/cvc5.opam
@@ -0,0 +1,33 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "OCaml bindings for the cvc5 SMT solver"
+description: "OCaml bindings for the cvc5 SMT solver"
+maintainer: ["João Pereira <joaomhmpereira@tecnico.ulisboa.pt>"]
+authors: ["João Pereira <joaomhmpereira@tecnico.ulisboa.pt>"]
+homepage: "https://github.com/formalsec/ocaml-cvc5"
+bug-reports: "https://github.com/formalsec/ocaml-cvc5/issues"
+depends: [
+  "dune" {>= "3.10"}
+  "ocaml" {>= "4.12"}
+  "conf-gcc" {build}
+  "conf-g++" {build}
+  "conf-gmp" {build}
+  "conf-cmake" {build}
+  "conf-python-3" {build}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/formalsec/ocaml-cvc5.git"
diff --git a/cvc5_external.ml b/cvc5_external.ml
index de23812..ed03944 100644
--- a/cvc5_external.ml
+++ b/cvc5_external.ml
@@ -3,68 +3,148 @@
 (** External declarations for cvc5's OCaml bindings. *)
 
 (**/**)
+
 type ptr
+
 and result = ptr
+
 and synth_result = ptr
+
 and sort = ptr
+
 and term = ptr
+
 and op = ptr
+
 and datatype = ptr
+
 and datatype_constructor_decl = ptr
+
 and datatype_decl = ptr
+
 and datatype_selector = ptr
+
 and datatype_constructor = ptr
+
 and grammar = ptr
+
 and solver = ptr
+
 and term_manager = ptr
+
 and option_info = ptr
+
 and proof = ptr
+
 and proof_rule = ptr
+
 and statistics = ptr
+
 and unknown_explanation = ptr
+
 and sort_kind = ptr
+
 and kind = ptr
+
 and rounding_mode = ptr
+
 and proof_format = ptr
+
 and proof_component = ptr
+
 and learned_lit_type = ptr
+
 and block_model_mode = ptr
+
 and find_synth_target = ptr
 
-external result_is_sat : result -> bool = "ocaml_cvc5_stub_result_is_sat" [@@noalloc]
-external result_is_unsat : result -> bool = "ocaml_cvc5_stub_result_is_unsat" [@@noalloc]
-external result_is_unknown : result -> bool = "ocaml_cvc5_stub_result_is_unknown" [@@noalloc]
+external result_is_sat : result -> bool = "ocaml_cvc5_stub_result_is_sat"
+[@@noalloc]
+
+external result_is_unsat : result -> bool = "ocaml_cvc5_stub_result_is_unsat"
+[@@noalloc]
+
+external result_is_unknown : result -> bool
+  = "ocaml_cvc5_stub_result_is_unknown"
+[@@noalloc]
+
 external mk_true : term_manager -> term = "ocaml_cvc5_stub_mk_true"
+
 external mk_false : term_manager -> term = "ocaml_cvc5_stub_mk_false"
+
 external mk_bool : term_manager -> bool -> term = "ocaml_cvc5_stub_mk_bool"
+
 external mk_int : term_manager -> int -> term = "ocaml_cvc5_stub_mk_int"
+
 external mk_bv : term_manager -> int -> int64 -> term = "ocaml_cvc5_stub_mk_bv"
+
 external mk_real : term_manager -> string -> term = "ocaml_cvc5_stub_mk_real"
-external mk_string : term_manager -> string -> term = "ocaml_cvc5_stub_mk_string"
-external mk_term : term_manager -> int -> term array -> term = "ocaml_cvc5_stub_mk_term"
-external get_boolean_sort : term_manager -> sort = "ocaml_cvc5_stub_get_boolean_sort"
-external get_integer_sort : term_manager -> sort = "ocaml_cvc5_stub_get_integer_sort"
+
+external mk_string : term_manager -> string -> term
+  = "ocaml_cvc5_stub_mk_string"
+
+external mk_term : term_manager -> int -> term array -> term
+  = "ocaml_cvc5_stub_mk_term"
+
+external get_boolean_sort : term_manager -> sort
+  = "ocaml_cvc5_stub_get_boolean_sort"
+
+external get_integer_sort : term_manager -> sort
+  = "ocaml_cvc5_stub_get_integer_sort"
+
 external get_real_sort : term_manager -> sort = "ocaml_cvc5_stub_get_real_sort"
-external get_string_sort : term_manager -> sort = "ocaml_cvc5_stub_get_string_sort"
-external mk_bitvector_sort : term_manager -> int -> sort = "ocaml_cvc5_stub_mk_bitvector_sort"
-external mk_const_s : term_manager -> sort -> string -> term = "ocaml_cvc5_stub_mk_const_s"
+
+external get_string_sort : term_manager -> sort
+  = "ocaml_cvc5_stub_get_string_sort"
+
+external mk_bitvector_sort : term_manager -> int -> sort
+  = "ocaml_cvc5_stub_mk_bitvector_sort"
+
+external mk_const_s : term_manager -> sort -> string -> term
+  = "ocaml_cvc5_stub_mk_const_s"
+
 external mk_const : term_manager -> sort -> term = "ocaml_cvc5_stub_mk_const"
-external mk_roundingmode : term_manager -> int -> term = "ocaml_cvc5_stub_mk_rounding_mode"
+
+external mk_roundingmode : term_manager -> int -> term
+  = "ocaml_cvc5_stub_mk_rounding_mode"
+
 external term_to_string : term -> string = "ocaml_cvc5_stub_term_to_string"
-external term_equal : term -> term -> bool = "ocaml_cvc5_stub_term_equal" [@@noalloc]
+
+external term_equal : term -> term -> bool = "ocaml_cvc5_stub_term_equal"
+[@@noalloc]
+
 external term_id : term -> int = "ocaml_cvc5_stub_term_id" [@@noalloc]
+
 external term_kind : term -> int = "ocaml_cvc5_stub_term_kind" [@@noalloc]
+
 external term_sort : term -> sort = "ocaml_cvc5_stub_term_sort"
+
 external new_solver : term_manager -> solver = "ocaml_cvc5_stub_new_solver"
-external new_term_manager : unit -> term_manager = "ocaml_cvc5_stub_new_term_manager"
-external delete_term_manager : term_manager -> unit = "ocaml_cvc5_stub_delete_term_manager"
+
+external new_term_manager : unit -> term_manager
+  = "ocaml_cvc5_stub_new_term_manager"
+
+external delete_term_manager : term_manager -> unit
+  = "ocaml_cvc5_stub_delete_term_manager"
+
 external delete : solver -> unit = "ocaml_cvc5_stub_delete"
-external assert_formula : solver -> term -> unit = "ocaml_cvc5_stub_assert_formula" [@@noalloc]
+
+external assert_formula : solver -> term -> unit
+  = "ocaml_cvc5_stub_assert_formula"
+[@@noalloc]
+
 external check_sat : solver -> result = "ocaml_cvc5_stub_check_sat"
-external set_logic : solver -> string -> unit = "ocaml_cvc5_stub_set_logic" [@@noalloc]
+
+external set_logic : solver -> string -> unit = "ocaml_cvc5_stub_set_logic"
+[@@noalloc]
+
 external simplify : solver -> term -> term = "ocaml_cvc5_stub_simplify"
+
 external push : solver -> int -> unit = "ocaml_cvc5_stub_push" [@@noalloc]
+
 external pop : solver -> int -> unit = "ocaml_cvc5_stub_pop" [@@noalloc]
-external reset_assertions : solver -> unit = "ocaml_cvc5_stub_reset_assertions" [@@noalloc]
 
-(**/**)
\ No newline at end of file
+external reset_assertions : solver -> unit = "ocaml_cvc5_stub_reset_assertions"
+[@@noalloc]
+
+(**/**)
diff --git a/dune b/dune
index 74ab8c8..8156784 100644
--- a/dune
+++ b/dune
@@ -1,30 +1,47 @@
-(executable
- (name toy)
- (libraries cvc5)
- (modules toy))
+(rule
+ (deps
+  (source_tree vendor))
+ (targets libpicpolyxx.a libpicpoly.a libcadical.a libcvc5.a cvc5_export.h)
+ (action
+  (no-infer
+   (progn
+    (chdir
+     vendor/cvc5
+     (progn
+      (run ./configure.sh --auto-download --static)
+      (run make -C build -j 4)))
+    (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a)
+    (copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a)
+    (copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a)
+    (copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a)
+    (copy
+     vendor/cvc5/build/include/cvc5/cvc5_export.h
+     vendor/cvc5/include/cvc5/cvc5_export.h)
+    (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h)))))
 
 (library
+ (public_name cvc5)
  (name cvc5)
  (modules cvc5 cvc5_enums cvc5_external)
- (foreign_stubs 
+ (no_dynlink)
+ (foreign_stubs
   (language cxx)
   (names cvc5_stubs)
+  (extra_deps cvc5_export.h)
   (flags :standard -std=c++17 -I/opt/homebrew/include)
-  (include_dirs 
-   vendor/cvc5/include
-   vendor/cvc5/src
-   vendor/cvc5/src/lib))
- (foreign_archives
-  vendor/cadical
-  vendor/cvc5
-  vendor/picpoly
-  vendor/picpolyxx)
+  (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib))
+ (foreign_archives cadical cvc5 picpoly picpolyxx)
  (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp))
 
 (rule
- (deps (:executable api/cvc5_enums.exe))
+ (deps ./api/cvc5_enums.exe)
  (target cvc5_enums.ml)
  (action
   (with-stdout-to
    %{target}
-   (run %{deps}))))
\ No newline at end of file
+   (run %{deps}))))
+
+(executable
+ (name toy)
+ (libraries cvc5)
+ (modules toy))
diff --git a/dune-project b/dune-project
index 0293f42..6a75bd5 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,25 @@
-(lang dune 3.7)
+(lang dune 3.10)
 
-(name cvc5_cxx)
\ No newline at end of file
+(name cvc5)
+
+(generate_opam_files true)
+
+(source
+ (github formalsec/ocaml-cvc5))
+
+(authors "João Pereira <joaomhmpereira@tecnico.ulisboa.pt>")
+
+(maintainers "João Pereira <joaomhmpereira@tecnico.ulisboa.pt>")
+
+(package
+  (name cvc5)
+  (synopsis "OCaml bindings for the cvc5 SMT solver")
+  (description "OCaml bindings for the cvc5 SMT solver")
+  (depends
+   dune
+   (ocaml (>= 4.12))
+   (conf-gcc :build)
+   (conf-g++ :build)
+   (conf-gmp :build)
+   (conf-cmake :build)
+   (conf-python-3 :build)))
diff --git a/toy.ml b/toy.ml
index 09fd03b..1611194 100644
--- a/toy.ml
+++ b/toy.ml
@@ -1,15 +1,19 @@
 open Cvc5
 
 let tm = TermManager.mk_tm ()
+
 let solver = Solver.mk_solver tm
+
 let int_sort = Sort.mk_int_sort tm
+
 let x = Term.mk_const_s tm int_sort "x"
+
 let zero = Term.mk_int tm 0
 
 let () =
-  let x_gt_zero = Term.mk_term tm Kind.Gt [|x; zero|] in
+  let x_gt_zero = Term.mk_term tm Kind.Gt [| x; zero |] in
   print_endline (Term.to_string x_gt_zero);
-  let x_lt_zero = Term.mk_term tm Kind.Lt [|zero; x|] in
+  let x_lt_zero = Term.mk_term tm Kind.Lt [| zero; x |] in
   print_endline (Term.to_string x_lt_zero);
   (* x > 0 *)
   Solver.assert_formula solver x_gt_zero;
@@ -21,4 +25,4 @@ let () =
   TermManager.delete_tm tm;
   match b with
   | true -> print_endline "sat OCaml"
-  | false -> print_endline "unsat OCaml" 
+  | false -> print_endline "unsat OCaml"
diff --git a/vendor/dune b/vendor/dune
deleted file mode 100644
index c961ee4..0000000
--- a/vendor/dune
+++ /dev/null
@@ -1,10 +0,0 @@
-(data_only_dirs cvc5)
-
-(rule
- (deps
-  (source_tree cvc5))
- (targets libcvc5.a libcadical.a libpicpoly.a libpicpolyxx.a)
- (action
-   (bash
-    "\ncd cvc5 && ./configure.sh --auto-download --static\ncd build && make\ncd ../../\ncp cvc5/build/src/libcvc5.a libcvc5.a\ncp cvc5/build/deps/lib/libcadical.a libcadical.a\n cp cvc5/build/deps/lib/libpicpoly.a libpicpoly.a\ncp cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a\n"))
-)
\ No newline at end of file