diff --git a/proofs/psnj_toolbox/bin/qfo.ml b/proofs/psnj_toolbox/bin/qfo.ml
index 3c9c304bc48486520d84967cbe6d91d9dc70d1d3..614257809f6ff18f7f4bc17586cddbb6b234a888 100644
--- a/proofs/psnj_toolbox/bin/qfo.ml
+++ b/proofs/psnj_toolbox/bin/qfo.ml
@@ -59,7 +59,12 @@ let new_sig_state (mp : Path.t) : Sig_state.t =
 
 let translate (config : string) (mapfile : string) (eval : string list) : unit =
   (* Get symbol mappings *)
-  let mapping = PsnjQfo.Mappings.of_file mapfile in
+  let mapping =
+    let ic = open_in mapfile in
+    let ret = PsnjQfo.Mappings.of_channel ic in
+    close_in ic;
+    ret
+  in
   let pvs_cert, pvs_connectives, propositional_connectives =
     let f s =
       try StrMap.find s mapping
diff --git a/proofs/psnj_toolbox/lib/qfo/dune b/proofs/psnj_toolbox/lib/qfo/dune
index 9a493de4446f5c8e4e7b36c589d9d1bd517d2585..e6867a1715403177b49b4dc21886390f0ccb1fbc 100644
--- a/proofs/psnj_toolbox/lib/qfo/dune
+++ b/proofs/psnj_toolbox/lib/qfo/dune
@@ -1,7 +1,7 @@
 (library
  (public_name personoj.qfo)
  (libraries
-  yojson
+  ezjsonm
   lambdapi.common
   lambdapi.lplib
   lambdapi.parsing
diff --git a/proofs/psnj_toolbox/lib/qfo/mappings.ml b/proofs/psnj_toolbox/lib/qfo/mappings.ml
index c1394737b7a549e77e46938a04e9ed77c4ae6ab4..70428a0efa3ac16932e860fe2a862d5acde11c76 100644
--- a/proofs/psnj_toolbox/lib/qfo/mappings.ml
+++ b/proofs/psnj_toolbox/lib/qfo/mappings.ml
@@ -2,7 +2,6 @@
      to work on. A symbol mapping specify which symbol of a Dedukti
      encoding implements such symbol. *)
 
-module J = Yojson.Basic
 open Lplib
 open Extra
 
@@ -10,14 +9,15 @@ type t = (string * string) list StrMap.t
 
 (** [parse obj] parses json object [obj] into a map from module names
     (as strings) to symbol mappings (as assoc list of strings). *)
-let parse (obj : J.t) : t =
-  let f (modl, map) =
-    let map =
-      J.Util.to_assoc map |> List.map (fun (x, y) -> (x, J.Util.to_string y))
+let parse (obj : Ezjsonm.t) : t =
+  let f (modl, builtins) =
+    let dict =
+      Ezjsonm.get_dict builtins
+      |> List.map (fun (k, v) -> (k, Ezjsonm.get_string v))
     in
-    StrMap.add modl map
+    StrMap.add modl dict
   in
-  List.fold_right f (J.Util.to_assoc obj) StrMap.empty
+  List.fold_right f Ezjsonm.(get_dict (value obj)) StrMap.empty
 
-(** [of_file src] parses the json object in file [src]. *)
-let of_file (src : string) : t = J.from_file src |> parse
+(** [of_file ic] parses the json object from channel [ic]. *)
+let of_channel (ic : in_channel) : t = Ezjsonm.from_channel ic |> parse
diff --git a/proofs/psnj_toolbox/lib/qfo/mappings.mli b/proofs/psnj_toolbox/lib/qfo/mappings.mli
index 2de04bdd469ac00f1479d3ea43a9143bb0d8fbc7..7e5d72b61640b01363b5560c60056bcd0ea33980 100644
--- a/proofs/psnj_toolbox/lib/qfo/mappings.mli
+++ b/proofs/psnj_toolbox/lib/qfo/mappings.mli
@@ -6,5 +6,5 @@ type t = (string * string) list StrMap.t
     ["propositional_connectives"]) to association from label
     (e.g. "truth") to a symbol name. See the manual page. *)
 
-val of_file : string -> t
-(** [of_file f] create a mapping from a file [f]. *)
+val of_channel : in_channel -> t
+(** [of_channel ic] create a mapping from channel [ic]. *)
diff --git a/proofs/psnj_toolbox/personoj.opam.locked b/proofs/psnj_toolbox/personoj.opam.locked
index 6aa761bd5665610a74ee5445505a650b31dfb0f6..7b4c46bacb8a16270a2441f8b0af5089deb915bc 100644
--- a/proofs/psnj_toolbox/personoj.opam.locked
+++ b/proofs/psnj_toolbox/personoj.opam.locked
@@ -17,10 +17,14 @@ depends: [
   "conf-pkg-config" {= "2"}
   "cppo" {= "1.6.8"}
   "csexp" {= "1.5.1"}
+  "cstruct" {= "6.0.1"}
   "dune" {= "2.9.1"}
   "dune-configurator" {= "2.9.1"}
   "easy-format" {= "1.3.2"}
+  "ezjsonm" {= "1.3.0"}
   "gen" {= "0.5.3"}
+  "hex" {= "1.4.0"}
+  "jsonm" {= "1.0.1"}
   "lambdapi" {= "1.0"}
   "menhir" {= "20211128"}
   "menhirLib" {= "20211128"}
@@ -44,7 +48,9 @@ depends: [
   "sexplib0" {= "v0.14.0"}
   "stdlib-shims" {= "0.3.0"}
   "timed" {= "1.0"}
+  "topkg" {= "1.0.4"}
   "uchar" {= "0.0.2"}
+  "uutf" {= "1.0.2"}
   "why3" {= "1.4.0"}
   "yojson" {= "1.7.0"}
 ]