diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index b4251e8d..405734a0 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -582,4 +582,7 @@ def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T)
   if s.len = src.len then ok src
   else fail panic
 
+/- [core::array::TryFromSliceError] -/
+def core.array.TryFromSliceError := ()
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean
index 02aff85f..f792e812 100644
--- a/backends/lean/Base/Primitives/Core.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -111,3 +111,43 @@ def core.convert.IntoFrom {T : Type} {U : Type} (fromInst : core.convert.From U
 def core.convert.FromSame (T : Type) : core.convert.From T T := {
   from_ := fun x => ok (core.convert.FromSame.from_ x)
 }
+
+/- [core::result::Result] -/
+inductive core.result.Result (T : Type) (E : Type) :=
+| Ok : T → core.result.Result T E
+| Err : E → core.result.Result T E
+
+/- [core::fmt::Error] -/
+@[reducible] def core.fmt.Error := Unit
+
+structure core.convert.TryFrom (Self T : Type) where
+  Error : Type
+  try_from : T → Result (core.result.Result Self Error)
+
+structure core.convert.TryInto (Self T : Type) where
+  Error : Type
+  try_into : Self → Result (core.result.Result T Error)
+
+@[reducible, simp]
+def core.convert.TryIntoFrom.try_into {T U : Type} (fromInst : core.convert.TryFrom U T)
+  (x : T) : Result (core.result.Result U fromInst.Error) :=
+  fromInst.try_from x
+
+@[reducible]
+def core.convert.TryIntoFrom {T U : Type} (fromInst : core.convert.TryFrom U T) :
+  core.convert.TryInto T U := {
+  Error := fromInst.Error
+  try_into := core.convert.TryIntoFrom.try_into fromInst
+}
+
+/- TODO: -/
+axiom Formatter : Type
+
+structure core.fmt.Debug (T : Type) where
+  fmt : T → Formatter → Result (Formatter × Formatter → Formatter)
+
+def core.result.Result.unwrap {T E : Type}
+  (_ : core.fmt.Debug T) (e : core.result.Result T E) : Primitives.Result T :=
+  match e with
+  | .Ok x => ok x
+  | .Err _ => fail .panic
diff --git a/src/Config.ml b/src/Config.ml
index d9fed408..7d315ca4 100644
--- a/src/Config.ml
+++ b/src/Config.ml
@@ -45,6 +45,9 @@ let if_backend (f : unit -> 'a) (default : 'a) : 'a =
   | None -> default
   | Some _ -> f ()
 
+(** Print all the external definitions which are not listed in the builtin functions *)
+let print_unknown_externals = ref false
+
 (** {1 Interpreter} *)
 
 (** Activate the sanity checks, and in particular the invariant checks
diff --git a/src/Errors.ml b/src/Errors.ml
index e66876c0..36d066d3 100644
--- a/src/Errors.ml
+++ b/src/Errors.ml
@@ -57,6 +57,16 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option)
 let craise (file : string) (line : int) (span : Meta.span) (msg : string) =
   craise_opt_span file line (Some span) msg
 
+(** Lazy assert *)
+let classert_opt_span (file : string) (line : int) (b : bool)
+    (span : Meta.span option) (msg : string Lazy.t) =
+  if not b then craise_opt_span file line span (Lazy.force msg)
+
+(** Lazy assert *)
+let classert (file : string) (line : int) (b : bool) (span : Meta.span)
+    (msg : string Lazy.t) =
+  classert_opt_span file line b (Some span) msg
+
 let cassert_opt_span (file : string) (line : int) (b : bool)
     (span : Meta.span option) (msg : string) =
   if not b then craise_opt_span file line span msg
diff --git a/src/Main.ml b/src/Main.ml
index 469ec647..fa624b7b 100644
--- a/src/Main.ml
+++ b/src/Main.ml
@@ -57,6 +57,37 @@ Usage: %s [OPTIONS] FILE
 |}
     Sys.argv.(0)
 
+let matches_name (c : crate) (name : Types.name)
+    (m : 'a ExtractName.NameMatcherMap.t) : bool =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = c.type_decls;
+      global_decls = c.global_decls;
+      fun_decls = c.fun_decls;
+      trait_decls = c.trait_decls;
+      trait_impls = c.trait_impls;
+    }
+  in
+  NameMatcherMap.mem mctx name m
+
+let matches_name_with_generics (c : crate) (name : Types.name)
+    (generics : Types.generic_args) (m : 'a ExtractName.NameMatcherMap.t) : bool
+    =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = c.type_decls;
+      global_decls = c.global_decls;
+      fun_decls = c.fun_decls;
+      trait_decls = c.trait_decls;
+      trait_impls = c.trait_impls;
+    }
+  in
+  Option.is_some (NameMatcherMap.find_with_generics_opt mctx name generics m)
+
 let () =
   (* Measure start time *)
   let start_time = Unix.gettimeofday () in
@@ -129,6 +160,10 @@ let () =
         Arg.Set use_nested_tuple_projectors,
         " Use nested projectors for tuples (e.g., (0, 1, 2).snd.fst instead of \
          (0, 1, 2).1)." );
+      ( "-print-unknown-externals",
+        Arg.Set print_unknown_externals,
+        " Print all the external definitions which are not listed in the \
+         builtin functions" );
     ]
   in
 
@@ -190,8 +225,6 @@ let () =
     if cond then fail_with_error msg
   in
 
-  if !print_llbc then main_log#set_level EL.Debug;
-
   (* Sanity check (now that the arguments are parsed!) *)
   check_arg_implies
     (not !extract_template_decreases_clauses)
@@ -300,7 +333,9 @@ let () =
   | Ok m ->
       (* Logging *)
       log#linfo (lazy ("Imported: " ^ filename));
-      log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
+      if !print_llbc then
+        log#linfo (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"))
+      else log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
 
       (* Check the Charon CLI options *)
       check_no_doc m.options.hide_marker_traits
@@ -323,6 +358,144 @@ let () =
            definitions";
         fail true);
 
+      (* Print the external definitions which are not listed in the builtin functions *)
+      if !print_unknown_externals then (
+        let open TranslateCore in
+        let { type_decls; fun_decls; global_decls; trait_decls; trait_impls; _ }
+            =
+          m
+        in
+        (* Filter the definitions *)
+        let type_decls =
+          Types.TypeDeclId.Map.filter
+            (fun _ (d : Types.type_decl) ->
+              let names_map = ExtractBuiltin.builtin_types_map () in
+              (not d.item_meta.is_local)
+              && not (matches_name m d.item_meta.name names_map))
+            type_decls
+        in
+        let fun_decls =
+          LlbcAst.FunDeclId.Map.filter
+            (fun _ (d : LlbcAst.fun_decl) ->
+              let names_map = ExtractBuiltin.builtin_funs_map () in
+              (not d.item_meta.is_local)
+              && (not (matches_name m d.item_meta.name names_map))
+              (* We also ignore the trait method declarations *)
+              &&
+              match d.kind with
+              | TraitDeclItem _ -> false
+              | _ -> true)
+            fun_decls
+        in
+        let global_decls =
+          LlbcAst.GlobalDeclId.Map.filter
+            (fun _ (d : LlbcAst.global_decl) ->
+              let funs_map = ExtractBuiltin.builtin_globals_map in
+              (not d.item_meta.is_local)
+              && not (matches_name m d.item_meta.name funs_map))
+            global_decls
+        in
+        let trait_decls =
+          LlbcAst.TraitDeclId.Map.filter
+            (fun _ (d : LlbcAst.trait_decl) ->
+              let names_map = ExtractBuiltin.builtin_trait_decls_map () in
+              (not d.item_meta.is_local)
+              && not (matches_name m d.item_meta.name names_map))
+            trait_decls
+        in
+        let trait_impls =
+          List.filter_map
+            (fun (d : LlbcAst.trait_impl) ->
+              let names_map = ExtractBuiltin.builtin_trait_impls_map () in
+              match
+                LlbcAst.TraitDeclId.Map.find_opt d.impl_trait.trait_decl_id
+                  m.trait_decls
+              with
+              | None -> None (* Just ignore it *)
+              | Some trait_decl ->
+                  if
+                    (not d.item_meta.is_local)
+                    && not
+                         (matches_name_with_generics m trait_decl.item_meta.name
+                            d.impl_trait.decl_generics names_map)
+                  then Some (d, trait_decl)
+                  else None)
+            (LlbcAst.TraitImplId.Map.values trait_impls)
+        in
+        (* Print *)
+        let fmt_env = Print.Crate.crate_to_fmt_env m in
+        let type_decls =
+          List.map
+            (fun (d : Types.type_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              "Type decl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.type_decl_to_string fmt_env d)
+            (Types.TypeDeclId.Map.values type_decls)
+        in
+        let fun_decls =
+          List.map
+            (fun (d : LlbcAst.fun_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              let d =
+                (* FIXME: there is a bug in the formatter when splitting the predicates
+                   and trait clauses between the inherited ones and the others (the
+                   index is sometimes out of bounds).
+                   See: https://github.com/AeneasVerif/charon/issues/482
+                *)
+                try Print.Ast.fun_decl_to_string fmt_env "" "  " d
+                with _ -> "UNKNOWN"
+              in
+              "Fun decl (pattern: [" ^ pattern ^ "]]):\n" ^ d)
+            (LlbcAst.FunDeclId.Map.values fun_decls)
+        in
+        let global_decls =
+          List.map
+            (fun (d : LlbcAst.global_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              "Global decl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.Ast.global_decl_to_string fmt_env "" "  " d)
+            (LlbcAst.GlobalDeclId.Map.values global_decls)
+        in
+        let trait_decls =
+          List.map
+            (fun (d : LlbcAst.trait_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              "Trait decl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.Ast.trait_decl_to_string fmt_env "" "  " d)
+            (LlbcAst.TraitDeclId.Map.values trait_decls)
+        in
+        let trait_impls =
+          List.map
+            (fun ((d, trait_decl) : LlbcAst.trait_impl * LlbcAst.trait_decl) ->
+              let pattern =
+                TranslateCore.name_with_generics_crate_to_pattern_string m
+                  trait_decl.item_meta.name trait_decl.generics
+                  d.impl_trait.decl_generics
+              in
+              "Trait impl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.Ast.trait_impl_to_string fmt_env "" "  " d)
+            trait_impls
+        in
+
+        log#linfo
+          (lazy
+            (String.concat "\n\n"
+               (type_decls @ fun_decls @ global_decls @ trait_decls
+              @ trait_impls)));
+        ());
+
       (* There may be exceptions to catch *)
       (try
          (* Apply the pre-passes *)
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 688cbe34..25b8b4fc 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -76,6 +76,43 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
   in
   name_with_generics_to_simple_name mctx ~prefix n p g
 
+let name_with_crate_to_pattern_string (ctx : LlbcAst.crate) (n : Types.name) :
+    string =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_decls;
+      global_decls = ctx.global_decls;
+      fun_decls = ctx.fun_decls;
+      trait_decls = ctx.trait_decls;
+      trait_impls = ctx.trait_impls;
+    }
+  in
+  let c : Charon.NameMatcher.to_pat_config =
+    { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let pat = Charon.NameMatcher.name_to_pattern mctx c n in
+  Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
+
+let name_with_generics_crate_to_pattern_string (ctx : LlbcAst.crate)
+    (n : Types.name) (params : Types.generic_params) (args : Types.generic_args)
+    : string =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_decls;
+      global_decls = ctx.global_decls;
+      fun_decls = ctx.fun_decls;
+      trait_decls = ctx.trait_decls;
+      trait_impls = ctx.trait_impls;
+    }
+  in
+  let c : Charon.NameMatcher.to_pat_config =
+    { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let pat =
+    Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args
+  in
+  Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
+
 let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string =
   let mctx : Charon.NameMatcher.ctx =
     {
diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml
index ca145577..6729d5c2 100644
--- a/src/extract/ExtractBase.ml
+++ b/src/extract/ExtractBase.ml
@@ -1680,10 +1680,13 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx)
     let clause_trait = clause.trait.binder_value in
     (* *)
     let trait_id = clause_trait.trait_decl_id in
-    let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
-    let args = clause_trait.decl_generics in
-    trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
-      impl_trait_decl.item_meta.name params args
+    (* The declaration may be missing because of an error *)
+    match TraitDeclId.Map.find_opt trait_id ctx.crate.trait_decls with
+    | None -> [ "clause" ]
+    | Some impl_trait_decl ->
+        let args = clause_trait.decl_generics in
+        trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
+          impl_trait_decl.item_meta.name params args
   in
   String.concat "" clause
 
diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml
index ea0802ef..c8a91e25 100644
--- a/src/extract/ExtractBuiltin.ml
+++ b/src/extract/ExtractBuiltin.ml
@@ -237,6 +237,13 @@ let builtin_types () : builtin_type_info list =
              ]);
     };
   ]
+  @ mk_lean_only
+      [
+        mk_type "core::fmt::Formatter" ();
+        mk_type "core::result::Result" ();
+        mk_type "core::fmt::Error" ();
+        mk_type "core::array::TryFromSliceError" ();
+      ]
 
 let mk_builtin_types_map () =
   NameMatcherMap.of_list
@@ -540,6 +547,7 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
            ~can_fail:false ~extract_name:(Some "core.convert.FromSame.from_") ();
          (* [core::slice::{@Slice<T>}::copy_from_slice] *)
          mk_fun "core::slice::{[@T]}::copy_from_slice" ();
+         mk_fun "core::result::{core::result::Result<@T, @E>}::unwrap" ();
        ]
       @ List.map
           (fun ty ->
@@ -705,6 +713,10 @@ let builtin_trait_decls_info () =
         (* Into *)
         mk_trait "core::convert::Into" ~types:[ "T"; "U" ] ~methods:[ "into" ]
           ();
+        (* Debug *)
+        mk_trait "core::fmt::Debug" ~types:[ "T" ] ~methods:[ "fmt" ] ();
+        mk_trait "core::convert::TryFrom" ~methods:[ "try_from" ] ();
+        mk_trait "core::convert::TryInto" ~methods:[ "try_into" ] ();
       ]
 
 let mk_builtin_trait_decls_map () =
@@ -795,6 +807,9 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
         (* From<T, T> *)
         fmt "core::convert::From<@Self, @Self>"
           ~extract_name:(Some "core::convert::FromSame") ();
+        (* TryInto<T, U : TryFrom<T>> *)
+        fmt "core::convert::{core::convert::TryInto<@T, @U>}"
+          ~extract_name:(Some "core::convert::TryIntoFrom") ();
       ]
   (* From<INT, bool> *)
   @ List.map
@@ -829,6 +844,15 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
             (Some ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty))
           ())
       all_int_names
+  (* Copy<INT> *)
+  @ List.map
+      (fun ty ->
+        fmt
+          ("core::marker::Copy<" ^ ty ^ ">")
+          ~extract_name:
+            (Some ("core.marker.Copy" ^ StringUtils.capitalize_first_letter ty))
+          ())
+      all_int_names
 
 let mk_builtin_trait_impls_map () =
   let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in
diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index 01172a1c..1ae92058 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -1185,9 +1185,15 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed
     (* For now we don't support nested borrows, so we check that there
        aren't parent regions *)
     let parents = list_ancestor_region_groups regions_hierarchy gid in
-    cassert_opt_span __FILE__ __LINE__
+    classert_opt_span __FILE__ __LINE__
       (T.RegionGroupId.Set.is_empty parents)
-      span "Nested borrows are not supported yet";
+      span
+      (lazy
+        (let ctx = Print.Contexts.decls_ctx_to_fmt_env decls_ctx in
+         "Nested borrows are not supported yet (found in the signature of: "
+         ^ Charon.PrintExpressions.fun_id_or_trait_method_ref_to_string ctx
+             fun_id
+         ^ ")"));
     (* For now, we don't allow nested borrows, so the additional inputs to the
        backward function can only come from borrows that were returned like
        in (for the backward function we introduce for 'a):
diff --git a/tests/lean/Builtin.lean b/tests/lean/Builtin.lean
index 4e2cb72d..65057344 100644
--- a/tests/lean/Builtin.lean
+++ b/tests/lean/Builtin.lean
@@ -9,17 +9,17 @@ set_option linter.unusedVariables false
 namespace builtin
 
 /- [builtin::clone_bool]:
-   Source: 'tests/src/builtin.rs', lines 5:0-7:1 -/
+   Source: 'tests/src/builtin.rs', lines 6:0-8:1 -/
 def clone_bool (x : Bool) : Result Bool :=
   Result.ok (core.clone.impls.CloneBool.clone x)
 
 /- [builtin::clone_u32]:
-   Source: 'tests/src/builtin.rs', lines 9:0-11:1 -/
+   Source: 'tests/src/builtin.rs', lines 10:0-12:1 -/
 def clone_u32 (x : U32) : Result U32 :=
   Result.ok (core.clone.impls.CloneU32.clone x)
 
 /- [builtin::into_from]:
-   Source: 'tests/src/builtin.rs', lines 13:0-15:1 -/
+   Source: 'tests/src/builtin.rs', lines 14:0-16:1 -/
 def into_from
   {T : Type} {U : Type} (coreconvertFromInst : core.convert.From U T) (x : T) :
   Result U
@@ -27,29 +27,35 @@ def into_from
   core.convert.IntoFrom.into coreconvertFromInst x
 
 /- [builtin::into_same]:
-   Source: 'tests/src/builtin.rs', lines 17:0-19:1 -/
+   Source: 'tests/src/builtin.rs', lines 18:0-20:1 -/
 def into_same {T : Type} (x : T) : Result T :=
   core.convert.IntoFrom.into (core.convert.FromSame T) x
 
 /- [builtin::from_same]:
-   Source: 'tests/src/builtin.rs', lines 21:0-23:1 -/
+   Source: 'tests/src/builtin.rs', lines 22:0-24:1 -/
 def from_same {T : Type} (x : T) : Result T :=
   Result.ok (core.convert.FromSame.from_ x)
 
 /- [builtin::copy]:
-   Source: 'tests/src/builtin.rs', lines 25:0-27:1 -/
+   Source: 'tests/src/builtin.rs', lines 26:0-28:1 -/
 def copy
   {T : Type} (coremarkerCopyInst : core.marker.Copy T) (x : T) : Result T :=
   Result.ok x
 
 /- [builtin::u32_from_le_bytes]:
-   Source: 'tests/src/builtin.rs', lines 29:0-31:1 -/
+   Source: 'tests/src/builtin.rs', lines 30:0-32:1 -/
 def u32_from_le_bytes (x : Array U8 4#usize) : Result U32 :=
   Result.ok (core.num.U32.from_le_bytes x)
 
 /- [builtin::u32_to_le_bytes]:
-   Source: 'tests/src/builtin.rs', lines 33:0-35:1 -/
+   Source: 'tests/src/builtin.rs', lines 34:0-36:1 -/
 def u32_to_le_bytes (x : U32) : Result (Array U8 4#usize) :=
   Result.ok (core.num.U32.to_le_bytes x)
 
+/- [builtin::use_debug_clause]:
+   Source: 'tests/src/builtin.rs', lines 38:0-38:49 -/
+def use_debug_clause
+  {T : Type} (corefmtDebugInst : core.fmt.Debug T) (t : T) : Result Unit :=
+  Result.ok ()
+
 end builtin
diff --git a/tests/src/builtin.rs b/tests/src/builtin.rs
index 4c70257a..6190ae93 100644
--- a/tests/src/builtin.rs
+++ b/tests/src/builtin.rs
@@ -1,3 +1,4 @@
+//@ charon-args=--exclude=core::fmt::Debug::fmt --opaque=core::fmt::Formatter
 //@[!lean] skip
 //! This file uses a list of builtin definitions, to make sure they are properly
 //! detected and mapped to definitions in the standard library.
@@ -33,3 +34,5 @@ fn u32_from_le_bytes(x: [u8; 4]) -> u32 {
 fn u32_to_le_bytes(x: u32) -> [u8; 4] {
     x.to_le_bytes()
 }
+
+fn use_debug_clause<T: core::fmt::Debug>(_: T) {}