diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Revision history for containers-verified
 
+## 0.6.0.1 -- 2018-06-18
+
+* Now also verified: `Set.map` and `Set.fromList` (#1)
+* Update proofs to `containers-0.6.0.1`
+
 ## 0.5.11.0 -- 2018-03-15
 
 * First version.
diff --git a/Data/Set.hs b/Data/Set.hs
--- a/Data/Set.hs
+++ b/Data/Set.hs
@@ -58,7 +58,7 @@
             , S.splitAt
 
 --          -- * Map
---          , S.map
+            , S.map
             , mapMonotonic
 
             -- * Folds
@@ -87,7 +87,7 @@
 --          -- ** List
             , elems
             , toList
---          , fromList
+            , fromList
 
 --          -- ** Ordered list
             , toAscList
diff --git a/containers-verified.cabal b/containers-verified.cabal
--- a/containers-verified.cabal
+++ b/containers-verified.cabal
@@ -1,5 +1,5 @@
 name:                containers-verified
-version:             0.5.11.0
+version:             0.6.0.1
 synopsis:            Formally verified drop-in replacement of containers
 description:
   In the context of the <https://deepspec.org/main DeepSpec project>, parts of the
@@ -24,14 +24,15 @@
   This package does not re-export any of the @….Internals@ modules.
   .
   We cannot control which type class instances are re-exported; these therefore
-  may give you access to unverified code. Also, the @conatiners@ code contains
+  may give you access to unverified code. Also, the @containers@ code contains
   some CPP directives; these can enable different code on your machine than the
   code that we verified (e.g. different bit-widths).
   .
   To learn more about what exactly has been verified, and how wide the
-  formalization gap is, see the paper “Ready, Set, Verify! Applying hs-to-coq
-  to non-trivial Haskell code” by Joachim Breitner, Antal Spector-Zabusky, Yao
-  Li, Christine Rizkallah, John Wiegley and Stephanie Weirich.
+  formalization gap is, see the paper
+  <https://arxiv.org/abs/1803.06960 “Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code”>
+  by Joachim Breitner, Antal Spector-Zabusky, Yao Li,
+  Christine Rizkallah, John Wiegley and Stephanie Weirich.
 
   .
   The long-term maintenance plan for this package is not fleshed out yet, and
@@ -51,12 +52,15 @@
 cabal-version:       >=1.10
 
 library
-  build-depends:       containers ==0.5.11.0
+  build-depends:       containers ==0.6.0.1
   default-language:    Haskell2010
   exposed-modules:
         Data.Set
         Data.IntSet
         Data.Map
+  -- The following ensures that GHCi will not complain about ambiguous module
+  -- names when both containers and containers-verified is in a project.
+  exposed: False
 
 source-repository head
     type:     git