diff --git a/proof-libs/fstar/core/Core.Fmt.fsti b/proof-libs/fstar/core/Core.Fmt.fsti
new file mode 100644
index 000000000..f8f29873b
--- /dev/null
+++ b/proof-libs/fstar/core/Core.Fmt.fsti
@@ -0,0 +1,3 @@
+module Core.Fmt
+
+val t_Arguments: Type0
diff --git a/proof-libs/fstar/core/Core.Mem.fsti b/proof-libs/fstar/core/Core.Mem.fsti
new file mode 100644
index 000000000..6618ab010
--- /dev/null
+++ b/proof-libs/fstar/core/Core.Mem.fsti
@@ -0,0 +1,5 @@
+module Core.Mem
+open Rust_primitives
+
+// FIXME(unsafe!): remove default type (see #545)
+val size_of (#[FStar.Tactics.exact (`eqtype_as_type unit)]t:Type): unit -> usize
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index 2b8401121..31bd7bc52 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -42,5 +42,5 @@ val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v ex
 val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.Error.t_ParseIntError
 
 val impl__usize__ilog2: i32 -> u32 
-
+val impl__usize__leading_zeros: usize -> u32