diff --git a/dune-project b/dune-project
index 6ec16743..db87e215 100644
--- a/dune-project
+++ b/dune-project
@@ -29,8 +29,10 @@
     (< 4.0)))
   (iter
    (>= 1.0))
+  (trace (>= 0.3))
   (zarith :with-test)
   (alcotest :with-test)
+  (trace-tef (and :with-test (>= 0.3)))
   (odoc :with-doc))
  (depopts
   (mtime
@@ -74,4 +76,6 @@
    (= :version))
   (sidekick-base
    (= :version))
-  menhir))
+  menhir)
+ (depopts
+   (trace-tef (>= 0.3))))
diff --git a/examples/sudoku/dune b/examples/sudoku/dune
index d3683a6e..2e1c73da 100644
--- a/examples/sudoku/dune
+++ b/examples/sudoku/dune
@@ -5,7 +5,7 @@
   sidekick.core
   sidekick.util
   sidekick.sat
-  sidekick.tef ; for profiling
+  trace-tef ; for profiling
   iter
   containers)
  (flags :standard -warn-error -a+8 -color always -safe-string
diff --git a/examples/sudoku/sudoku_solve.ml b/examples/sudoku/sudoku_solve.ml
index 1343087d..88bca0aa 100644
--- a/examples/sudoku/sudoku_solve.ml
+++ b/examples/sudoku/sudoku_solve.ml
@@ -311,7 +311,7 @@ end = struct
   type t = { grid0: Grid.t; tst: Term.store; theory: Theory.t; solver: Sat.t }
 
   let solve (self : t) : _ option =
-    let@ () = Profile.with_ "sudoku.solve" in
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "sudoku.solve" in
     let assumptions =
       Grid.all_cells self.grid0
       |> Iter.filter (fun (_, _, c) -> Cell.is_full c)
@@ -359,7 +359,7 @@ let chrono ~pp_time : (module CHRONO) =
   (module M)
 
 let solve_file ~use_stats ~pp_time file =
-  let@ () = Profile.with_ "solve-file" in
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "solve-file" in
   let open (val chrono ~pp_time) in
   Format.printf "solve grids in file %S@." file;
 
@@ -401,7 +401,7 @@ let solve_file ~use_stats ~pp_time file =
   ()
 
 let () =
-  let@ () = Sidekick_tef.with_setup in
+  let@ () = Trace_tef.with_setup () in
   Fmt.set_color_default true;
   let files = ref [] in
   let debug = ref 0 in
diff --git a/examples/sudoku/tests/dune b/examples/sudoku/tests/dune
index 26685776..733b5a35 100644
--- a/examples/sudoku/tests/dune
+++ b/examples/sudoku/tests/dune
@@ -8,5 +8,6 @@
 
 (rule
  (alias runtest)
+ (package sidekick)
  (action
   (diff head15_top1465.expected head15_top1465.out)))
diff --git a/sidekick-bin.opam b/sidekick-bin.opam
index 3fa436d2..8d231daf 100644
--- a/sidekick-bin.opam
+++ b/sidekick-bin.opam
@@ -14,6 +14,9 @@ depends: [
   "sidekick-base" {= version}
   "menhir"
 ]
+depopts: [
+  "trace-tef" {>= "0.3"}
+]
 build: [
   ["dune" "subst"] {pinned}
   [
diff --git a/sidekick.opam b/sidekick.opam
index 671080eb..db0a9397 100644
--- a/sidekick.opam
+++ b/sidekick.opam
@@ -12,8 +12,10 @@ depends: [
   "dune" {>= "2.0"}
   "containers" {>= "3.6" & < "4.0"}
   "iter" {>= "1.0"}
+  "trace" {>= "0.3"}
   "zarith" {with-test}
   "alcotest" {with-test}
+  "trace-tef" {with-test & >= "0.3"}
   "odoc" {with-doc}
 ]
 depopts: [
diff --git a/src/algos/simplex/sidekick_simplex.ml b/src/algos/simplex/sidekick_simplex.ml
index 83c6d096..ed93f682 100644
--- a/src/algos/simplex/sidekick_simplex.ml
+++ b/src/algos/simplex/sidekick_simplex.ml
@@ -652,6 +652,8 @@ module Make (Arg : ARG) :
      See page 14, figure 3.1 *)
   let pivot_and_update (self : t) (x_i : var_state) (x_j : var_state) (v : erat)
       : unit =
+    Profile.messagef (fun k ->
+        k "pivot x_i=%a x_j=%a" V.pp x_i.var V.pp x_j.var);
     assert (Var_state.is_basic x_i);
     assert (Var_state.is_n_basic x_j);
     _check_invariants_internal self;
diff --git a/src/bin-lib/Sidekick_bin_lib.ml b/src/bin-lib/Sidekick_bin_lib.ml
index 4d615d2a..55987a11 100644
--- a/src/bin-lib/Sidekick_bin_lib.ml
+++ b/src/bin-lib/Sidekick_bin_lib.ml
@@ -4,3 +4,4 @@ module Dimacs_lexer = Dimacs_lexer
 module Dimacs_parser = Dimacs_parser
 module Drup_lexer = Drup_lexer
 module Drup_parser = Drup_parser
+module Trace_setup = Trace_setup
diff --git a/src/bin-lib/dune b/src/bin-lib/dune
index b8cdc863..e52ade26 100644
--- a/src/bin-lib/dune
+++ b/src/bin-lib/dune
@@ -2,7 +2,10 @@
  (name sidekick_bin_lib)
  (public_name sidekick-bin.lib)
  (synopsis "Utils for the sidekick binaries")
- (libraries containers sidekick.util)
+ (libraries containers sidekick.util
+            (select trace_setup.ml from
+              (trace-tef -> trace_setup.real.ml)
+              (-> trace_setup.dummy.ml)))
  (flags :standard -warn-error -a+8 -open Sidekick_util))
 
 (ocamllex
diff --git a/src/bin-lib/trace_setup.dummy.ml b/src/bin-lib/trace_setup.dummy.ml
new file mode 100644
index 00000000..5d7a7553
--- /dev/null
+++ b/src/bin-lib/trace_setup.dummy.ml
@@ -0,0 +1 @@
+let with_trace f = f ()
diff --git a/src/bin-lib/trace_setup.mli b/src/bin-lib/trace_setup.mli
new file mode 100644
index 00000000..00cb0f63
--- /dev/null
+++ b/src/bin-lib/trace_setup.mli
@@ -0,0 +1,2 @@
+
+val with_trace : (unit -> 'a) -> 'a
diff --git a/src/bin-lib/trace_setup.real.ml b/src/bin-lib/trace_setup.real.ml
new file mode 100644
index 00000000..fae82415
--- /dev/null
+++ b/src/bin-lib/trace_setup.real.ml
@@ -0,0 +1 @@
+let with_trace f = Trace_tef.with_setup () f
diff --git a/src/cc/CC.ml b/src/cc/CC.ml
index 577519dd..00148c3e 100644
--- a/src/cc/CC.ml
+++ b/src/cc/CC.ml
@@ -218,7 +218,7 @@ exception E_confl of Result_action.conflict
 
 let raise_conflict_ (cc : t) ~th (e : Lit.t list) (p : Sidekick_proof.Step.id) :
     _ =
-  Profile.instant "cc.conflict";
+  Profile.message "cc.conflict";
   (* clear tasks queue *)
   Vec.clear cc.pending;
   Vec.clear cc.combine;
diff --git a/src/checker/drup_check.ml b/src/checker/drup_check.ml
index ed9b4664..1f576800 100644
--- a/src/checker/drup_check.ml
+++ b/src/checker/drup_check.ml
@@ -69,7 +69,7 @@ end = struct
 
   (* check event, return [true] if it's valid *)
   let check_op (self : t) i (op : Trace.op) : bool =
-    Profile.with_ "check-op" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "check-op" in
     Log.debugf 20 (fun k -> k "(@[check-op :idx %d@ :op %a@])" i Trace.pp_op op);
 
     match op with
diff --git a/src/checker/dune b/src/checker/dune
index 78cda5a4..3be7dcee 100644
--- a/src/checker/dune
+++ b/src/checker/dune
@@ -2,6 +2,6 @@
  (name main)
  (public_name sidekick-checker)
  (package sidekick-bin)
- (libraries containers sidekick-bin.lib sidekick.util sidekick.tef
+ (libraries containers sidekick-bin.lib sidekick.util
    sidekick.drup)
  (flags :standard -warn-error -a+8 -open Sidekick_util))
diff --git a/src/checker/main.ml b/src/checker/main.ml
index a7622fcb..855c54af 100644
--- a/src/checker/main.ml
+++ b/src/checker/main.ml
@@ -6,7 +6,7 @@ let clause_of_int_l store atoms : Drup_check.clause =
   |> Drup_check.Clause.of_iter store
 
 let check ?pb proof : bool =
-  Profile.with_ "check" @@ fun () ->
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "check" in
   let cstore = Drup_check.Clause.create () in
   let trace = Drup_check.Trace.create cstore in
 
@@ -14,7 +14,7 @@ let check ?pb proof : bool =
   (match pb with
   | None -> ()
   | Some f when Filename.extension f = ".cnf" ->
-    Profile.with_ "parse-pb.cnf" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "parse-pb.cnf" in
     CCIO.with_in f (fun ic ->
         let parser_ = BL.Dimacs_parser.create ic in
         BL.Dimacs_parser.iter parser_ (fun atoms ->
@@ -42,11 +42,11 @@ let check ?pb proof : bool =
   (match proof with
   | f when Filename.extension f = ".drup" ->
     (* read file *)
-    Profile.with_ "parse-proof.drup" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "parse-proof.drup" in
     CCIO.with_in f add_proof_from_chan
   | f when Filename.extension f = ".gz" ->
     (* read compressed proof *)
-    Profile.with_ "parse-proof.drup" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "parse-proof.drup" in
     (* TODO: more graceful failure mode here *)
     assert (Filename.extension @@ Filename.chop_extension f = ".drup");
     let cmd = Printf.sprintf "gzip --keep -d -c \"%s\"" f in
@@ -70,7 +70,7 @@ let () =
   let files = ref [] in
   let opts = [ "-d", Arg.Int Log.set_debug, " set debug level" ] |> Arg.align in
   Printexc.record_backtrace true;
-  Sidekick_tef.setup ();
+  let@ () = Sidekick_bin_lib.Trace_setup.with_trace in
 
   let t1 = Unix.gettimeofday () in
 
diff --git a/src/drup/sidekick_drup.ml b/src/drup/sidekick_drup.ml
index 895bf1d5..64ccaeac 100644
--- a/src/drup/sidekick_drup.ml
+++ b/src/drup/sidekick_drup.ml
@@ -364,7 +364,7 @@ module Make () : S = struct
     (* perform boolean propagation in a fixpoint
        @raise Conflict if a clause is false *)
     let bcp_fixpoint_ (self : t) : unit =
-      Profile.with_ "bcp-fixpoint" @@ fun () ->
+      let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "bcp-fixpoint" in
       while self.trail_ptr < Atom.Stack.size self.trail do
         let a = Atom.Stack.get self.trail self.trail_ptr in
         Log.debugf 50 (fun k -> k "(@[bcp@ :atom %a@])" Atom.pp a);
diff --git a/src/main/dune b/src/main/dune
index 8e519ff3..ded0b3a3 100644
--- a/src/main/dune
+++ b/src/main/dune
@@ -7,7 +7,7 @@
  (modules main pure_sat_solver)
  (modes native)
  (libraries containers iter result sidekick.sat sidekick.core sidekick-base
-   sidekick.smt-solver sidekick-base.smtlib sidekick.tef sidekick.drup
+   sidekick.smt-solver sidekick-base.smtlib sidekick.drup
    sidekick.memtrace sidekick-bin.lib)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
diff --git a/src/main/main.ml b/src/main/main.ml
index 93ee9861..ae76d0b2 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -211,7 +211,10 @@ let main_smt ~config () : _ result =
     Solver.Smt_solver.Solver.add_theory solver Sidekick_smtlib.Check_cc.theory;
 
   let parse_res =
-    let@ () = Profile.with_ "parse" ~args:[ "file", !file ] in
+    let@ _sp =
+      Profile.with_span ~__FILE__ ~__LINE__ "parse" ~data:(fun () ->
+          [ "file", `String !file ])
+    in
     Sidekick_smtlib.parse tst !file
   in
 
@@ -252,7 +255,7 @@ let main () =
   Sys.catch_break true;
 
   (* instrumentation and tracing *)
-  Sidekick_tef.with_setup @@ fun () ->
+  let@ () = Sidekick_bin_lib.Trace_setup.with_trace in
   Sidekick_memtrace.trace_if_requested ~context:"sidekick" ();
 
   CCFormat.set_color_default true;
diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml
index dd047d6a..f78ebf74 100644
--- a/src/main/pure_sat_solver.ml
+++ b/src/main/pure_sat_solver.ml
@@ -150,7 +150,10 @@ let tracer ~(sink : Tr.Sink.t) () : SAT.Tracer.t =
 let start = Sys.time ()
 
 let solve ?check:(_ = false) (solver : SAT.t) : (unit, string) result =
-  let res = Profile.with_ "solve" (fun () -> SAT.solve solver) in
+  let res =
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "solve" in
+    SAT.solve solver
+  in
   let t2 = Sys.time () in
   Printf.printf "\r";
   flush stdout;
diff --git a/src/quip/Sidekick_quip.ml b/src/quip/Sidekick_quip.ml
index a6096d9b..1a2cc425 100644
--- a/src/quip/Sidekick_quip.ml
+++ b/src/quip/Sidekick_quip.ml
@@ -143,7 +143,7 @@ module Make_printer (Out : OUT) = struct
   (* toplevel wrapper *)
   let pp self : printer =
    fun out ->
-    Profile.with_ "quip.print" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "quip.print" in
     l [ a "quip"; a "1"; pp_rec self ] out
 
   let pp_debug self : printer = pp self
diff --git a/src/sat/solver.ml b/src/sat/solver.ml
index b3fd08e5..d9a6f775 100644
--- a/src/sat/solver.ml
+++ b/src/sat/solver.ml
@@ -419,9 +419,10 @@ let clause_bump_activity self (c : clause) : unit =
   )
 
 let emit_counters_ (self : t) =
-  if Profile.enabled () then
-    Profile.count "sat"
-      [ "decisions", decision_level self; "trail", AVec.size self.trail ]
+  if Profile.enabled () then (
+    Profile.counter_int "sat.decisions" (decision_level self);
+    Profile.counter_int "sat.trail" (AVec.size self.trail)
+  )
 
 (* Simplification of clauses.
 
@@ -1658,7 +1659,7 @@ let pick_branch_lit ~full self : bool =
 (* do some amount of search, until the number of conflicts or clause learnt
    reaches the given parameters *)
 let search (self : t) ~on_progress ~(max_conflicts : int) : unit =
-  let@ () = Profile.with_ "sat.search" in
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "sat.search" in
   Log.debugf 3 (fun k ->
       k "(@[sat.search@ :max-conflicts %d@ :max-learnt %d@])" max_conflicts
         !(self.max_clauses_learnt));
@@ -1683,7 +1684,7 @@ let search (self : t) ~on_progress ~(max_conflicts : int) : unit =
       assert (self.elt_head = AVec.size self.trail);
       assert (self.elt_head = self.th_head);
       if max_conflicts > 0 && !n_conflicts >= max_conflicts then (
-        Profile.instant "sat.restart";
+        Profile.message "sat.restart";
         Log.debug 1 "(sat.restarting)";
         cancel_until self 0;
         Stat.incr self.n_restarts;
@@ -1721,7 +1722,7 @@ let[@inline] eval st lit = fst @@ eval_level st lit
 (* fixpoint of propagation and decisions until a model is found, or a
    conflict is reached *)
 let solve_ ~on_progress (self : t) : unit =
-  let@ () = Profile.with_ "sat.solve" in
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "sat.solve" in
   Log.debugf 5 (fun k ->
       k "(@[sat.solve :assms %d@])" (AVec.size self.assumptions));
   check_unsat_ self;
@@ -1767,7 +1768,7 @@ let solve_ ~on_progress (self : t) : unit =
           Clause.iter self.store c ~f:(fun a ->
               insert_var_order self (Atom.var a));
 
-          Profile.instant "sat.th-conflict";
+          Profile.message "sat.th-conflict";
           Log.debugf 5 (fun k ->
               k "(@[sat.theory-conflict-clause@ %a@])" (Clause.debug self.store)
                 c);
diff --git a/src/smt/solver.ml b/src/smt/solver.ml
index d0123f55..6fff6c9a 100644
--- a/src/smt/solver.ml
+++ b/src/smt/solver.ml
@@ -141,11 +141,10 @@ let add_clause_nopreproc_ ~internal (self : t) (c : lit array) (proof : step_id)
   reset_last_res_ self;
   Log.debugf 50 (fun k ->
       k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c);
-  let pb = Profile.begin_ "add-clause" in
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "add-clause" in
   Sat_solver.add_clause_a self.solver
     (c :> lit array)
-    (fun () -> Proof.Pterm.ref proof);
-  Profile.exit pb
+    (fun () -> Proof.Pterm.ref proof)
 
 let add_clause_nopreproc_l_ ~internal self c p =
   add_clause_nopreproc_ ~internal self (CCArray.of_list c) p
@@ -181,7 +180,7 @@ let add_ty (self : t) ty = SI.add_ty self.si ~ty
 
 let solve ?(on_exit = []) ?(on_progress = fun _ -> ())
     ?(should_stop = fun _ -> false) ~assumptions (self : t) : res =
-  let@ () = Profile.with_ "smt-solver.solve" in
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "smt-solver.solve" in
   let do_on_exit () = List.iter (fun f -> f ()) on_exit in
 
   let on_progress =
diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml
index 96ed7ce1..b3c5cac8 100644
--- a/src/smt/solver_internal.ml
+++ b/src/smt/solver_internal.ml
@@ -328,7 +328,7 @@ let rec pop_lvls_theories_ n = function
 
 (* make model from the congruence closure *)
 let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
-  let@ () = Profile.with_ "smt-solver.mk-model" in
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "smt-solver.mk-model" in
   Log.debug 1 "(smt.solver.mk-model)";
   let module MB = Model_builder in
   let { cc; tst; model_ask = model_ask_hooks; model_complete; _ } = self in
@@ -483,19 +483,20 @@ let[@inline] iter_atoms_ (acts : theory_actions) : _ Iter.t =
   let (module A) = acts in
   A.iter_assumptions f
 
-(* propagation from the bool solver *)
+(** propagation from the bool solver *)
 let check_ ~final (self : t) (acts : sat_acts) =
-  let pb =
+  let[@inline] with_trace () f =
     if final then
-      Profile.begin_ "solver.final-check"
+      let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "solver.final-check" in
+      f ()
     else
-      Profile.null_probe
+      f ()
   in
+  let@ () = with_trace () in
   let iter = iter_atoms_ acts in
   Log.debugf 5 (fun k -> k "(smt-solver.assume :len %d)" (Iter.length iter));
   Event.emit self.on_progress ();
-  assert_lits_ ~final self acts iter;
-  Profile.exit pb
+  assert_lits_ ~final self acts iter
 
 (* propagation from the bool solver *)
 let[@inline] partial_check (self : t) (acts : Sidekick_sat.acts) : unit =
diff --git a/src/smtlib/Driver.ml b/src/smtlib/Driver.ml
index fc3a1b60..63479070 100644
--- a/src/smtlib/Driver.ml
+++ b/src/smtlib/Driver.ml
@@ -94,7 +94,7 @@ let solve (self : t) ~assumptions () : Solver.res =
   in
 
   let res =
-    let@ () = Profile.with_ "process.solve" in
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "process.solve" in
     Asolver.solve ~assumptions ?on_progress ~should_stop self.solver ()
   in
   let t2 = now () in
@@ -153,7 +153,7 @@ let known_logics =
 
 (* process a single statement *)
 let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
-  let@ () = Profile.with_ "smtlib.process-stmt" in
+  let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "smtlib.process-stmt" in
   Log.debugf 5 (fun k ->
       k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt);
 
diff --git a/src/smtlib/dune b/src/smtlib/dune
index c2be7ab2..a945a77b 100644
--- a/src/smtlib/dune
+++ b/src/smtlib/dune
@@ -4,5 +4,5 @@
  (synopsis "SMTLIB 2.6 driver for Sidekick")
  (private_modules Common_)
  (libraries containers zarith sidekick.core sidekick.util sidekick-base
-   sidekick.abstract-solver sidekick.mini-cc smtlib-utils sidekick.tef)
+   sidekick.abstract-solver sidekick.mini-cc smtlib-utils)
  (flags :standard -warn-error -a+8 -open Sidekick_util))
diff --git a/src/tef/Sidekick_tef.dummy.ml b/src/tef/Sidekick_tef.dummy.ml
deleted file mode 100644
index 7129c483..00000000
--- a/src/tef/Sidekick_tef.dummy.ml
+++ /dev/null
@@ -1,3 +0,0 @@
-let setup () = ()
-let teardown () = ()
-let with_setup f = f ()
diff --git a/src/tef/Sidekick_tef.mli b/src/tef/Sidekick_tef.mli
deleted file mode 100644
index 8766d4a6..00000000
--- a/src/tef/Sidekick_tef.mli
+++ /dev/null
@@ -1,24 +0,0 @@
-(** {1 Tracing Event Format}
-
-    A nice profiling format based on json, useful for visualizing what goes on.
-    It provides a backend for {!Sidekick_util.Profile} so that
-    profiling probes will emit TEF events.
-
-    Profiling is enabled if {!setup} is called, and if
-    the environment variable "TRACE" is set to "1" or "true".
-    The trace is emitted in the file "trace.json.gz" in the directory
-    where the solver is launched; you can open it in
-    chrome/chromium at "chrome://tracing".
-
-    {{: https://github.com/wolfpld/tracy} Tracy} can import (uncompressed)
-    trace files with a nice native trace explorer.
-
-    See {{: https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/}
-          the documentation of TEF}
-*)
-
-val setup : unit -> unit
-(** Install the TEF logger as a profiling backend. *)
-
-val teardown : unit -> unit
-val with_setup : (unit -> 'a) -> 'a
diff --git a/src/tef/Sidekick_tef.real.ml b/src/tef/Sidekick_tef.real.ml
deleted file mode 100644
index 61e698f8..00000000
--- a/src/tef/Sidekick_tef.real.ml
+++ /dev/null
@@ -1,130 +0,0 @@
-module P = Sidekick_util.Profile
-
-let active =
-  lazy
-    (match Sys.getenv "TRACE" with
-    | "1" | "true" -> true
-    | _ -> false
-    | exception Not_found -> false)
-
-let program_start = Mtime_clock.now ()
-
-module Make () : P.BACKEND = struct
-  let first_ = ref true
-  let closed_ = ref false
-
-  let teardown_ oc =
-    if not !closed_ then (
-      closed_ := true;
-      output_char oc ']';
-      (* close array *)
-      flush oc;
-      close_out_noerr oc
-    )
-
-  (* connection to subprocess writing into the file *)
-  let oc =
-    let oc = open_out_bin "trace.json" in
-    output_char oc '[';
-    at_exit (fun () -> teardown_ oc);
-    oc
-
-  let get_ts () : float =
-    let now = Mtime_clock.now () in
-    Mtime.Span.to_float_ns (Mtime.span program_start now) /. 1e3
-
-  let emit_sep_ () =
-    if !first_ then
-      first_ := false
-    else
-      output_string oc ",\n"
-
-  let char = output_char
-  let raw_string = output_string
-  let int oc i = Printf.fprintf oc "%d" i
-
-  let str_val oc (s : string) =
-    char oc '"';
-    let encode_char c =
-      match c with
-      | '"' -> raw_string oc {|\"|}
-      | '\\' -> raw_string oc {|\\|}
-      | '\n' -> raw_string oc {|\n|}
-      | '\b' -> raw_string oc {|\b|}
-      | '\r' -> raw_string oc {|\r|}
-      | '\t' -> raw_string oc {|\t|}
-      | _ when Char.code c <= 0x1f ->
-        raw_string oc {|\u00|};
-        Printf.fprintf oc "%02x" (Char.code c)
-      | c -> char oc c
-    in
-    String.iter encode_char s;
-    char oc '"'
-
-  (* emit args, if not empty. [ppv] is used to print values. *)
-  let emit_args_o_ ppv oc args : unit =
-    if args <> [] then (
-      Printf.fprintf oc {json|,"args": {|json};
-      List.iteri
-        (fun i (n, value) ->
-          if i > 0 then Printf.fprintf oc ",";
-          Printf.fprintf oc {json|"%s":%a|json} n ppv value)
-        args;
-      char oc '}'
-    )
-
-  let emit_duration_event ~name ~start ~end_ ~args () : unit =
-    let dur = end_ -. start in
-    let ts = start in
-    let pid = Unix.getpid () in
-    let tid = Thread.id (Thread.self ()) in
-    emit_sep_ ();
-    Printf.fprintf oc
-      {json|{"pid": %d,"cat":"","tid": %d,"dur": %.2f,"ts": %.2f,"name":%a,"ph":"X"%a}|json}
-      pid tid dur ts str_val name (emit_args_o_ str_val) args;
-    ()
-
-  let emit_instant_event ~name ~ts ~args () : unit =
-    let pid = Unix.getpid () in
-    let tid = Thread.id (Thread.self ()) in
-    emit_sep_ ();
-    Printf.fprintf oc
-      {json|{"pid": %d,"cat":"","tid": %d,"ts": %.2f,"name":%a,"ph":"I"%a}|json}
-      pid tid ts str_val name (emit_args_o_ str_val) args;
-    ()
-
-  let emit_count_event ~name ~ts (cs : _ list) : unit =
-    let pid = Unix.getpid () in
-    let tid = Thread.id (Thread.self ()) in
-    emit_sep_ ();
-    Printf.fprintf oc
-      {json|{"pid": %d,"cat":"","tid": %d,"ts": %.2f,"name":%a,"ph":"C"%a}|json}
-      pid tid ts str_val name (emit_args_o_ int) cs;
-    ()
-
-  let teardown () = teardown_ oc
-end
-
-let setup_ =
-  lazy
-    (let (lazy active) = active in
-     let b =
-       if active then
-         Some (module Make () : P.BACKEND)
-       else
-         None
-     in
-     P.Control.setup b)
-
-let setup () = Lazy.force setup_
-let teardown = P.Control.teardown
-
-let[@inline] with_setup f =
-  setup ();
-  try
-    let x = f () in
-    teardown ();
-    x
-  with e ->
-    teardown ();
-    raise e
diff --git a/src/tef/dune b/src/tef/dune
deleted file mode 100644
index 6e5aeb30..00000000
--- a/src/tef/dune
+++ /dev/null
@@ -1,15 +0,0 @@
-(library
- (name sidekick_tef)
- (public_name sidekick.tef)
- (synopsis "profiling backend based on TEF")
- (flags :standard -warn-error -a+8)
- (libraries
-  sidekick.util
-  unix
-  threads
-  (select
-   Sidekick_tef.ml
-   from
-   (mtime mtime.clock.os -> Sidekick_tef.real.ml)
-   (-> Sidekick_tef.dummy.ml)))
- (optional))
diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index fb548bc1..5fe0bab2 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -712,7 +712,7 @@ end = struct
      need it. *)
   let on_final_check (self : t) (solver : SI.t) (acts : SI.theory_actions)
       _trail =
-    Profile.with_ "data.final-check" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "data.final-check" in
     (* acyclicity check first *)
     Acyclicity_.check self solver acts;
 
@@ -736,7 +736,7 @@ end = struct
       Log.debugf 10 (fun k ->
           k "(@[%s.final-check.must-decide@ %a@])" name (Util.pp_list E_node.pp)
             l);
-      Profile.instant "data.case-split";
+      Profile.message "data.case-split";
       List.iter (decide_class_ self solver acts) l);
     ()
 
diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml
index ad08c927..33c3a3f4 100644
--- a/src/th-lra/sidekick_th_lra.ml
+++ b/src/th-lra/sidekick_th_lra.ml
@@ -499,7 +499,10 @@ module Make (A : ARG) = (* : S with module A = A *) struct
 
   (* raise conflict from certificate *)
   let fail_with_cert (self : state) si acts cert : 'a =
-    Profile.with1 "lra.simplex.check-cert" SimpSolver._check_cert cert;
+    (let@ _sp =
+       Profile.with_span ~__FILE__ ~__LINE__ "lra.simplex.check-cert"
+     in
+     SimpSolver._check_cert cert);
     let confl =
       SimpSolver.Unsat_cert.lits cert
       |> CCList.flat_map (Tag.to_lits si)
@@ -527,7 +530,14 @@ module Make (A : ARG) = (* : S with module A = A *) struct
           (SimpSolver.n_vars self.simplex)
           (SimpSolver.n_rows self.simplex));
     let res =
-      Profile.with_ "lra.simplex.solve" @@ fun () ->
+      let@ _sp =
+        Profile.with_span ~__FILE__ ~__LINE__ "lra.simplex.solve"
+          ~data:(fun () ->
+            [
+              "nvars", `Int (SimpSolver.n_vars self.simplex);
+              "nrows", `Int (SimpSolver.n_rows self.simplex);
+            ])
+      in
       SimpSolver.check self.simplex ~on_propagate:(on_propagate_ self si acts)
     in
     Log.debug 5 "(lra.check-simplex.done)";
@@ -666,7 +676,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
   (* partial checks is where we add literals from the trail to the
      simplex. *)
   let partial_check_ self si acts trail : unit =
-    Profile.with_ "lra.partial-check" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "lra.partial-check" in
     reset_res_ self;
     let changed = ref false in
 
@@ -679,7 +689,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
   let final_check_ (self : state) si (acts : SI.theory_actions)
       (trail : _ Iter.t) : unit =
     Log.debug 5 "(th-lra.final-check)";
-    Profile.with_ "lra.final-check" @@ fun () ->
+    let@ _sp = Profile.with_span ~__FILE__ ~__LINE__ "lra.final-check" in
     reset_res_ self;
 
     let changed = ref false in
diff --git a/src/util/Log.ml b/src/util/Log.ml
index 0a116641..de9a126a 100644
--- a/src/util/Log.ml
+++ b/src/util/Log.ml
@@ -1,7 +1,6 @@
 (** {1 Logging functions, real version} *)
 
 let enabled = true (* NOTE: change here for 0-overhead? *)
-
 let debug_level_ = ref 0
 let set_debug l = debug_level_ := l
 let get_debug () = !debug_level_
@@ -20,7 +19,7 @@ let[@inline never] debug_real_ l k =
         Format.fprintf _fmt "@]@?";
         let msg = Buffer.contents buf_ in
         (* forward to profiling *)
-        if Profile.enabled () then Profile.instant msg;
+        if Profile.enabled () then Profile.message msg;
         Format.fprintf !debug_fmt_ "@[<2>@{<Blue>[%d|%.3f]@}@ %s@]@." l now msg
       in
 
diff --git a/src/util/Profile.ml b/src/util/Profile.ml
index cc43cc8c..56845171 100644
--- a/src/util/Profile.ml
+++ b/src/util/Profile.ml
@@ -1,110 +1 @@
-module type BACKEND = sig
-  val get_ts : unit -> float
-
-  val emit_duration_event :
-    name:string ->
-    start:float ->
-    end_:float ->
-    args:(string * string) list ->
-    unit ->
-    unit
-
-  val emit_instant_event :
-    name:string -> ts:float -> args:(string * string) list -> unit -> unit
-
-  val emit_count_event : name:string -> ts:float -> (string * int) list -> unit
-  val teardown : unit -> unit
-end
-
-type backend = (module BACKEND)
-type probe = No_probe | Probe of { name: string; start: float }
-
-let null_probe = No_probe
-
-(* where to print events *)
-let out_ : backend option ref = ref None
-
-let[@inline] enabled () =
-  match !out_ with
-  | Some _ -> true
-  | None -> false
-
-let[@inline never] begin_with_ (module B : BACKEND) name : probe =
-  Probe { name; start = B.get_ts () }
-
-let[@inline] begin_ name : probe =
-  match !out_ with
-  | None -> No_probe
-  | Some b -> begin_with_ b name
-
-let[@inline] instant ?(args = []) name =
-  match !out_ with
-  | None -> ()
-  | Some (module B) ->
-    let now = B.get_ts () in
-    B.emit_instant_event ~name ~ts:now ~args ()
-
-let[@inline] count name cs =
-  if cs <> [] then (
-    match !out_ with
-    | None -> ()
-    | Some (module B) ->
-      let now = B.get_ts () in
-      B.emit_count_event ~name ~ts:now cs
-  )
-
-(* slow path *)
-let[@inline never] exit_full_ (module B : BACKEND) ~args name start =
-  let now = B.get_ts () in
-  B.emit_duration_event ~name ~start ~end_:now ~args ()
-
-let[@inline] exit_with_ ~args b pb =
-  match pb with
-  | No_probe -> ()
-  | Probe { name; start } -> exit_full_ ~args b name start
-
-let[@inline] exit ?(args = []) pb =
-  match pb, !out_ with
-  | Probe { name; start }, Some b -> exit_full_ ~args b name start
-  | _ -> ()
-
-let[@inline] with_ ?(args = []) name f =
-  match !out_ with
-  | None -> f ()
-  | Some b ->
-    let pb = begin_with_ b name in
-    (try
-       let x = f () in
-       exit_with_ ~args b pb;
-       x
-     with e ->
-       exit_with_ ~args b pb;
-       raise e)
-
-let[@inline] with1 ?(args = []) name f x =
-  match !out_ with
-  | None -> f x
-  | Some b ->
-    let pb = begin_with_ b name in
-    (try
-       let res = f x in
-       exit_with_ ~args b pb;
-       res
-     with e ->
-       exit_with_ ~args b pb;
-       raise e)
-
-let[@inline] with2 ?args name f x y = with_ ?args name (fun () -> f x y)
-
-module Control = struct
-  let setup b =
-    assert (!out_ = None);
-    out_ := b
-
-  let teardown () =
-    match !out_ with
-    | None -> ()
-    | Some (module B) ->
-      out_ := None;
-      B.teardown ()
-end
+include Trace_core
diff --git a/src/util/Profile.mli b/src/util/Profile.mli
deleted file mode 100644
index b44a9cc8..00000000
--- a/src/util/Profile.mli
+++ /dev/null
@@ -1,45 +0,0 @@
-(** Profiling probes.
-
-   This basic library can produce Catapult traces (a json file)
-   that can be read at [http://ui.perfetto.dev].
- *)
-
-type probe
-
-val null_probe : probe
-val enabled : unit -> bool
-val instant : ?args:(string * string) list -> string -> unit
-val begin_ : string -> probe
-val exit : ?args:(string * string) list -> probe -> unit
-val with_ : ?args:(string * string) list -> string -> (unit -> 'a) -> 'a
-val with1 : ?args:(string * string) list -> string -> ('a -> 'b) -> 'a -> 'b
-
-val with2 :
-  ?args:(string * string) list -> string -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
-
-val count : string -> (string * int) list -> unit
-
-module type BACKEND = sig
-  val get_ts : unit -> float
-
-  val emit_duration_event :
-    name:string ->
-    start:float ->
-    end_:float ->
-    args:(string * string) list ->
-    unit ->
-    unit
-
-  val emit_instant_event :
-    name:string -> ts:float -> args:(string * string) list -> unit -> unit
-
-  val emit_count_event : name:string -> ts:float -> (string * int) list -> unit
-  val teardown : unit -> unit
-end
-
-type backend = (module BACKEND)
-
-module Control : sig
-  val setup : backend option -> unit
-  val teardown : unit -> unit
-end
diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml
index d1509ab4..07d90a99 100644
--- a/src/util/Sidekick_util.ml
+++ b/src/util/Sidekick_util.ml
@@ -26,4 +26,4 @@ module Chunk_stack = Chunk_stack
 module Ser_value = Ser_value
 module Ser_decode = Ser_decode
 
-let[@inline] ( let@ ) f x = f x
+let ( let@ ) = ( @@ )
diff --git a/src/util/dune b/src/util/dune
index 44b960dc..557e2bbd 100644
--- a/src/util/dune
+++ b/src/util/dune
@@ -2,4 +2,4 @@
  (name sidekick_util)
  (public_name sidekick.util)
  (flags :standard -warn-error -a+8)
- (libraries containers iter sidekick.sigs bigarray unix))
+ (libraries containers iter sidekick.sigs bigarray unix trace.core))