diff --git a/src/goblint.ml b/src/goblint.ml
index 4ea3a3d242..15ef633016 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -21,6 +21,7 @@ let main () =
         allocated = true;
         count = true;
         tef = true;
+        tracy = false;
       };
       Timing.Program.start {
         cputime = false;
@@ -28,6 +29,7 @@ let main () =
         allocated = false;
         count = false;
         tef = true;
+        tracy = true;
       }
     );
 
diff --git a/src/util/timing/dune b/src/util/timing/dune
index 1a90c9bc12..c2635d1bd8 100644
--- a/src/util/timing/dune
+++ b/src/util/timing/dune
@@ -3,4 +3,4 @@
 (library
  (name goblint_timing)
  (public_name goblint.timing)
- (libraries catapult catapult-file))
+ (libraries catapult catapult-file tracy-client))
diff --git a/src/util/timing/goblint_timing.ml b/src/util/timing/goblint_timing.ml
index a65ce0ecf4..06c02f8d53 100644
--- a/src/util/timing/goblint_timing.ml
+++ b/src/util/timing/goblint_timing.ml
@@ -7,6 +7,7 @@ let dummy_options: options = {
   allocated = false;
   count = false;
   tef = false;
+  tracy = false;
 }
 
 (** TEF process ID for the next {!Make}.
@@ -41,6 +42,7 @@ struct
     start_walltime: float; (** Wall time at the beginning of the frame. *)
     start_allocated: float; (** Allocated memory at the beginning of the frame. *)
     (* No need for count, because it always gets incremented by 1. *)
+    tracy_span: Tracy_client.span;
   }
 
   let current_cputime (): float =
@@ -60,6 +62,7 @@ struct
       start_cputime = if !options.cputime then current_cputime () else 0.0;
       start_walltime = if !options.walltime then current_walltime () else 0.0;
       start_allocated = if !options.allocated then current_allocated () else 0.0;
+      tracy_span = -1;
     }
 
   (** Stack of currently active timing frames. *)
@@ -108,7 +111,14 @@ struct
       in
       loop tree.children
     in
-    Stack.push (create_frame tree) current;
+    let frame = create_frame tree in
+    let frame =
+      if !options.tracy then
+        {frame with tracy_span = Tracy_client.enter ~__FILE__ ~__LINE__ name}
+      else
+        frame
+    in
+    Stack.push frame current;
     if !options.tef then
       Catapult.Tracing.begin' ~pid:tef_pid ?args name
 
@@ -134,7 +144,9 @@ struct
     assert (tree.name = name);
     add_frame_to_tree frame tree;
     if !options.tef then
-      Catapult.Tracing.exit' ~pid:tef_pid name
+      Catapult.Tracing.exit' ~pid:tef_pid name;
+    if !options.tracy then
+      Tracy_client.exit frame.tracy_span
 
   let wrap ?args name f x =
     enter ?args name;
diff --git a/src/util/timing/goblint_timing_intf.ml b/src/util/timing/goblint_timing_intf.ml
index e41d33d6b8..304dd675d8 100644
--- a/src/util/timing/goblint_timing_intf.ml
+++ b/src/util/timing/goblint_timing_intf.ml
@@ -12,6 +12,7 @@ type options = {
   allocated: bool; (** Measure allocated memory. *)
   count: bool; (** Count calls. *)
   tef: bool; (** Output a TEF track. *)
+  tracy: bool;
 }
 
 (** Timing tree node. *)