diff --git a/creusot-contracts/src/model.rs b/creusot-contracts/src/model.rs
index b047053b8b..b9f50019e4 100644
--- a/creusot-contracts/src/model.rs
+++ b/creusot-contracts/src/model.rs
@@ -1,6 +1,5 @@
-use ::std::{rc::Rc, sync::Arc};
-
 use crate::*;
+use ::std::sync::Arc;
 
 /// The view of a type is its logical model as typically used to specify a data
 /// structure. It is typically "shallow", and does not involve the model of
@@ -29,24 +28,6 @@ pub trait DeepModel {
     fn deep_model(self) -> Self::DeepModelTy;
 }
 
-impl<T: DeepModel> DeepModel for Rc<T> {
-    type DeepModelTy = T::DeepModelTy;
-    #[logic]
-    #[open]
-    fn deep_model(self) -> Self::DeepModelTy {
-        pearlite! { self.view().deep_model() }
-    }
-}
-
-impl<T> View for Rc<T> {
-    type ViewTy = T;
-    #[logic]
-    #[trusted]
-    fn view(self) -> Self::ViewTy {
-        dead
-    }
-}
-
 impl View for str {
     type ViewTy = Seq<char>;
 
diff --git a/creusot-contracts/src/std.rs b/creusot-contracts/src/std.rs
index 08c5948870..0143fc5a6e 100644
--- a/creusot-contracts/src/std.rs
+++ b/creusot-contracts/src/std.rs
@@ -18,6 +18,7 @@ pub mod ops;
 pub mod option;
 pub mod panicking;
 pub mod ptr;
+pub mod rc;
 pub mod result;
 pub mod slice;
 pub mod string;
diff --git a/creusot-contracts/src/std/rc.rs b/creusot-contracts/src/std/rc.rs
new file mode 100644
index 0000000000..edb3930a4e
--- /dev/null
+++ b/creusot-contracts/src/std/rc.rs
@@ -0,0 +1,36 @@
+use crate::*;
+use ::std::{alloc::Allocator, rc::Rc};
+
+impl<T: DeepModel, A: Allocator> DeepModel for Rc<T, A> {
+    type DeepModelTy = T::DeepModelTy;
+    #[logic]
+    #[open]
+    fn deep_model(self) -> Self::DeepModelTy {
+        pearlite! { self.view().deep_model() }
+    }
+}
+
+impl<T, A: Allocator> View for Rc<T, A> {
+    type ViewTy = T;
+    #[logic]
+    #[trusted]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+extern_spec! {
+    mod std {
+        mod rc {
+            impl<T> Rc<T> {
+                #[ensures(result@ == value)]
+                fn new(value: T) -> Self;
+            }
+
+            impl<T, A: Allocator> AsRef for Rc<T, A> {
+                #[ensures(*result == (*self)@)]
+                fn as_ref(&self) -> &T;
+            }
+        }
+    }
+}