diff --git a/bv-sized.cabal b/bv-sized.cabal
--- a/bv-sized.cabal
+++ b/bv-sized.cabal
@@ -1,5 +1,5 @@
 name:                bv-sized
-version:             1.0.1
+version:             1.0.2
 category:            Bit Vectors
 synopsis:            a bitvector datatype that is parameterized by the vector width
 description:
@@ -45,7 +45,7 @@
                        bytestring,
                        hedgehog,
                        parameterized-utils,
-                       tasty >= 1.2.3 && < 1.3,
+                       tasty >= 1.2.3 && < 1.4,
                        tasty-hedgehog >= 1.0.0.2 && < 1.1
   default-language:    Haskell2010
   ghc-options:         -Wall -Wcompat
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,5 +1,15 @@
 # Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized)
 
+## 1.0.2 *August 2020*
+
+* Allows tasty 1.3 for test suite
+* Fixes bug in signedClamp function which made it possible to violate
+  the nonnegative invariant on the internal representation of BVs
+* Fixes divide by zero error in rotateL and rotateR
+* Enhances test suite to test well-formedness of all operators that
+  return a BV
+* Fixes some documentation
+
 ## 1.0.1 *May 2020*
 
 This fixed a subtle bug in the test suite which occasionally caused a
diff --git a/src/Data/BitVector/Sized.hs b/src/Data/BitVector/Sized.hs
--- a/src/Data/BitVector/Sized.hs
+++ b/src/Data/BitVector/Sized.hs
@@ -43,6 +43,7 @@
   , unsignedClamp, signedClamp
   , minUnsigned, maxUnsigned
   , minSigned, maxSigned
+  , zero, one, width
     -- * Construction from fixed-width data types
   , bool
   , word8, word16, word32, word64
@@ -62,7 +63,6 @@
   , and, or, xor
   , complement
   , shl, lshr, ashr, rotateL, rotateR
-  , zero, one, width
   , bit, bit'
   , setBit, setBit'
   , clearBit, clearBit'
@@ -108,7 +108,7 @@
 import Prelude (Integer)
 
 -- | Get the underlying 'Integer' representation from a 'BV'. We
--- guarantee that @(\\(BV.BV x) -> x) == BV.toUnsigned@.
+-- guarantee that @(\\(BV.BV x) -> x) == BV.asUnsigned@.
 pattern BV :: Integer -> BV.BV w
 pattern BV x <- BV.BV x
 {-# COMPLETE BV #-}
diff --git a/src/Data/BitVector/Sized/Internal.hs b/src/Data/BitVector/Sized/Internal.hs
--- a/src/Data/BitVector/Sized/Internal.hs
+++ b/src/Data/BitVector/Sized/Internal.hs
@@ -178,6 +178,18 @@
            -> Maybe (BV w)
 mkBVSigned w x = checkNatRepr w $ BV <$> signedToUnsigned w x
 
+-- | The zero bitvector of any width.
+zero :: NatRepr w -> BV w
+zero w = checkNatRepr w $ BV 0
+
+-- | The bitvector with value 1, of any positive width.
+one :: 1 <= w => NatRepr w -> BV w
+one w = checkNatRepr w $ BV 1
+
+-- | The bitvector whose value is its own width, of any width.
+width :: NatRepr w -> BV w
+width w = checkNatRepr w $ BV (intValue w)
+
 -- | The minimum unsigned value for bitvector with given width (always 0).
 minUnsigned :: NatRepr w -> BV w
 minUnsigned w = checkNatRepr w $ BV 0
@@ -206,9 +218,9 @@
 -- @-2^(w-1)@ and @2^(w-1) - 1@ (inclusive).
 signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w
 signedClamp w x = checkNatRepr w $
-  if | x < P.minSigned w -> BV (P.minSigned w)
+  if | x < P.minSigned w -> mkBV' w (P.minSigned w)
      | x > P.maxSigned w -> BV (P.maxSigned w)
-     | otherwise -> BV x
+     | otherwise -> mkBV' w x
 
 ----------------------------------------
 -- Construction from fixed-width data types
@@ -469,7 +481,7 @@
 -- | Bitwise rotate left.
 rotateL :: NatRepr w -> BV w -> Natural -> BV w
 rotateL w bv rot' = leftChunk `or` rightChunk
-  where rot = rot' `mod` wNatural
+  where rot = if wNatural == 0 then 0 else rot' `mod` wNatural
         leftChunk = shl w bv rot
         rightChunk = lshr w bv (wNatural - rot)
         wNatural = natValue w
@@ -477,22 +489,10 @@
 -- | Bitwise rotate right.
 rotateR :: NatRepr w -> BV w -> Natural -> BV w
 rotateR w bv rot' = leftChunk `or` rightChunk
-  where rot = rot' `mod` wNatural
+  where rot = if wNatural == 0 then 0 else rot' `mod` wNatural
         rightChunk = lshr w bv rot
         leftChunk = shl w bv (wNatural - rot)
         wNatural = natValue w
-
--- | The zero bitvector of any width.
-zero :: NatRepr w -> BV w
-zero w = checkNatRepr w $ BV 0
-
--- | The bitvector with value 1, of any positive width.
-one :: 1 <= w => NatRepr w -> BV w
-one w = checkNatRepr w $ BV 1
-
--- | The bitvector whose value is its own width, of any width.
-width :: NatRepr w -> BV w
-width w = checkNatRepr w $ BV (intValue w)
 
 -- | The 'BV' that has a particular bit set, and is 0 everywhere
 -- else.
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 
@@ -25,6 +26,7 @@
 import Data.Parameterized.Some
 import Data.Parameterized.Pair
 import Data.Word
+import Numeric.Natural
 
 ----------------------------------------
 -- Utilities
@@ -129,6 +131,43 @@
 smallPosWidth :: Gen (Some NatRepr)
 smallPosWidth = mkNatRepr <$> (Gen.integral $ Range.linear 1 4)
 
+data NatReprLte w where
+  NatReprLte :: (i <= w) => NatRepr i -> NatReprLte w
+
+deriving instance Show (NatReprLte w)
+
+natReprLte :: NatRepr w -> Gen (NatReprLte w)
+natReprLte w = do
+  n <- Gen.integral $ Range.linear 0 (natValue w)
+  Some i <- return $ mkNatRepr n
+  Just LeqProof <- return $ i `testLeq` w
+  return $ NatReprLte i
+
+data NatReprLt w where
+  NatReprLt :: (i+1 <= w) => NatRepr i -> NatReprLt w
+
+deriving instance Show (NatReprLt w)
+
+natReprLt :: NatRepr w -> Gen (NatReprLt w)
+natReprLt w = do
+  n <- Gen.integral $ Range.linear 0 (natValue w - 1)
+  Some i <- return $ mkNatRepr n
+  NatCaseLT LeqProof <- return $ i `testNatCases` w
+  return $ NatReprLt i
+
+data NatReprPosLt w where
+  NatReprPosLt :: (1 <= i, i+1 <= w) => NatRepr i -> NatReprPosLt w
+
+deriving instance Show (NatReprPosLt w)
+
+natReprPosLt :: NatRepr w -> Gen (NatReprPosLt w)
+natReprPosLt w = do
+  n <- Gen.integral $ Range.linear 1 (natValue w - 1)
+  Some i <- return $ mkNatRepr n
+  NatCaseLT LeqProof <- return $ i `testNatCases` w
+  Right LeqProof <- return $ isZeroOrGT1 i
+  return $ NatReprPosLt i
+
 bytes :: Gen [Word8]
 bytes = Gen.list (Range.linear 0 16) $ Gen.word8 Range.linearBounded
 
@@ -334,12 +373,274 @@
     deserTest (BS.pack <$> bytes) ((*8) . BS.length) BV.bytestringLE BV.asBytestringLE
   ]
 
+checkBounds :: MonadTest m => Integer -> NatRepr w -> m ()
+checkBounds x w = do
+  diff 0 (<=) x
+  diff x (<=) (2 ^ natValue w)
+
+wfCtor :: Gen (Some NatRepr)
+       -- ^ generator for width
+       -> (forall w . NatRepr w -> Integer -> Maybe (BV.BV w))
+       -- ^ constructor
+       -> Property
+wfCtor genW ctor = property $ do
+  Some w <- forAll genW
+  x <- forAll (largeSigned w)
+
+  case ctor w x of
+    Just (BV.BV x') -> checkBounds x' w
+    Nothing -> return ()
+
+wfCtor' :: NatRepr w
+        -- ^ fixed width of constructor
+        -> (Integer -> BV.BV w)
+        -- ^ embedding of integer into constructor arg
+        -> Property
+wfCtor' w ctor = property $ do
+  x <- forAll (largeSigned w)
+
+  let BV.BV x' = ctor x
+
+  checkBounds x' w
+
+wfUnary :: Gen (Some NatRepr)
+        -- ^ generator for width
+        -> (forall w . NatRepr w -> BV.BV w -> BV.BV w)
+        -- ^ unary operator
+        -> Property
+wfUnary genW op = property $ do
+  Some w <- forAll genW
+  bv <- BV.mkBV w <$> forAll (unsigned w)
+
+  let BV.BV x' = op w bv
+  checkBounds x' w
+
+wfUnaryMaybe :: Gen (Some NatRepr)
+             -- ^ generator for width
+             -> (forall w . NatRepr w -> BV.BV w -> Maybe (BV.BV w))
+             -- ^ unary operator
+             -> Property
+wfUnaryMaybe genW op = property $ do
+  Some w <- forAll genW
+  bv <- BV.mkBV w <$> forAll (unsigned w)
+
+  case op w bv of
+    Just (BV.BV x') -> checkBounds x' w
+    Nothing -> return ()
+
+wfBinary :: Gen (Some NatRepr)
+         -- ^ generator for width
+         -> (forall w . NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)
+         -- ^ binary operator
+         -> Property
+wfBinary genW op = property $ do
+  Some w <- forAll genW
+  bv1 <- BV.mkBV w <$> forAll (unsigned w)
+  bv2 <- BV.mkBV w <$> forAll (unsigned w)
+
+  let BV.BV x' = op w bv1 bv2
+  checkBounds x' w
+
+wfBinaryDiv :: Gen (Some NatRepr)
+            -- ^ generator for width
+            -> (forall w . NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)
+            -- ^ binary division-like operator
+            -> Property
+wfBinaryDiv genW op = property $ do
+  Some w <- forAll genW
+  bv1 <- BV.mkBV w <$> forAll (unsigned w)
+  bv2 <- BV.mkBV w <$> forAll (unsignedPos w)
+
+  let BV.BV x' = op w bv1 bv2
+  checkBounds x' w
+
+wfBinaryN :: Gen (Some NatRepr)
+          -- ^ generator for width
+          -> (forall w . NatRepr w -> BV.BV w -> Natural -> BV.BV w)
+          -- ^ binary operator with Natural arg
+          -> Property
+wfBinaryN genW op = property $ do
+  Some w <- forAll genW
+  bv <- BV.mkBV w <$> forAll (unsigned w)
+  n <- fromInteger <$> forAll (largeUnsigned w)
+
+  let BV.BV x' = op w bv n
+  checkBounds x' w
+
+wfBit :: Gen (Some NatRepr)
+      -- ^ generator for width
+      -> (forall w ix . ix+1 <= w => NatRepr w -> NatRepr ix -> BV.BV w -> BV.BV w)
+      -- ^ bit twiddling function
+      -> Property
+wfBit genW f = property $ do
+  Some w <- forAll genW
+  bv <- BV.mkBV w <$> forAll (unsigned w)
+  NatReprLt ix <- forAll (natReprLt w)
+
+  let BV.BV x = f w ix bv
+  checkBounds x w
+
+wfBitN :: Gen (Some NatRepr)
+       -- ^ generator for width
+       -> (forall w . NatRepr w -> Natural -> BV.BV w -> BV.BV w)
+       -- ^ bit twiddling function
+       -> Property
+wfBitN genW f = property $ do
+  Some w <- forAll genW
+  bv <- BV.mkBV w <$> forAll (unsigned w)
+  n <- fromInteger <$> forAll (largeUnsigned w)
+
+  let BV.BV x = f w n bv
+  checkBounds x w
+
+wellFormedTests :: TestTree
+wellFormedTests = testGroup "well-formedness tests"
+  [ testProperty "mkBV" $ wfCtor anyWidth (fmap Just . BV.mkBV)
+  , testProperty "mkBVUnsigned" $ wfCtor anyWidth BV.mkBVUnsigned
+  , testProperty "mkBVSigned" $ wfCtor anyPosWidth (forcePos BV.mkBVSigned)
+  , testProperty "signedClamp" $ wfCtor anyPosWidth (fmap Just . forcePos BV.signedClamp)
+  , testProperty "minUnsigned" $ wfCtor anyWidth (\w _ -> Just (BV.minUnsigned w))
+  , testProperty "maxUnsigned" $ wfCtor anyWidth (\w _ -> Just (BV.maxUnsigned w))
+  , testProperty "minSigned" $ wfCtor anyPosWidth (\w _ -> Just (forcePos BV.minSigned w))
+  , testProperty "maxSigned" $ wfCtor anyPosWidth (\w _ -> Just (forcePos BV.maxSigned w))
+  , testProperty "bool" $ wfCtor' knownNat (BV.bool . odd)
+  , testProperty "word8" $ wfCtor' knownNat (BV.word8 . fromInteger)
+  , testProperty "word16" $ wfCtor' knownNat (BV.word16 . fromInteger)
+  , testProperty "word32" $ wfCtor' knownNat (BV.word32 . fromInteger)
+  , testProperty "word64" $ wfCtor' knownNat (BV.word64 . fromInteger)
+  , testProperty "int8" $ wfCtor' knownNat (BV.int8 . fromInteger)
+  , testProperty "int16" $ wfCtor' knownNat (BV.int16 . fromInteger)
+  , testProperty "int32" $ wfCtor' knownNat (BV.int32 . fromInteger)
+  , testProperty "int64" $ wfCtor' knownNat (BV.int64 . fromInteger)
+  , testProperty "and" $ wfBinary anyWidth (const BV.and)
+  , testProperty "or" $ wfBinary anyWidth (const BV.or)
+  , testProperty "xor" $ wfBinary anyWidth (const BV.xor)
+  , testProperty "complement" $ wfUnary anyWidth BV.complement
+  , testProperty "shl" $ wfBinaryN anyWidth BV.shl
+  , testProperty "ashr" $ wfBinaryN anyPosWidth (forcePos BV.ashr)
+  , testProperty "lshr" $ wfBinaryN anyWidth BV.lshr
+  , testProperty "rotateL" $ wfBinaryN anyWidth BV.rotateL
+  , testProperty "rotateR" $ wfBinaryN anyWidth BV.rotateR
+  , testProperty "bit" $ property $ do
+      Some w <- forAll anyPosWidth
+      NatReprLt i <- forAll (natReprLt w)
+
+      let BV.BV x = BV.bit w i
+      checkBounds x w
+  , testProperty "bit'" $ property $ do
+      Some w <- forAll anyPosWidth
+      n <- forAll $ Gen.integral $ Range.linear 0 (2 * natValue w)
+
+      let BV.BV x = BV.bit' w n
+      checkBounds x w
+  , testProperty "setBit" $ wfBit anyPosWidth (const BV.setBit)
+  , testProperty "setBit'" $ wfBitN anyPosWidth BV.setBit'
+  , testProperty "clearBit" $ wfBit anyPosWidth BV.clearBit
+  , testProperty "clearBit'" $ wfBitN anyPosWidth BV.clearBit'
+  , testProperty "complementBit" $ wfBit anyPosWidth (const BV.complementBit)
+  , testProperty "complementBit'" $ wfBitN anyPosWidth BV.complementBit'
+  , testProperty "popCount" $ wfUnary anyWidth (const BV.popCount)
+  , testProperty "ctz" $ wfUnary anyWidth BV.ctz
+  , testProperty "clz" $ wfUnary anyWidth BV.clz
+  , testProperty "truncBits" $ property $ do
+      Some w <- forAll anyWidth
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+      n <- forAll $ Gen.integral $ Range.linear 0 (2 * natValue w)
+
+      let BV.BV x = BV.truncBits n bv
+      checkBounds x w
+  , testProperty "add" $ wfBinary anyWidth BV.add
+  , testProperty "sub" $ wfBinary anyWidth BV.sub
+  , testProperty "mul" $ wfBinary anyWidth BV.mul
+  , testProperty "uquot" $ wfBinaryDiv anyPosWidth (const BV.uquot)
+  , testProperty "urem" $ wfBinaryDiv anyPosWidth (const BV.urem)
+  , testProperty "squot" $ wfBinaryDiv anyPosWidth (forcePos BV.squot)
+  , testProperty "srem" $ wfBinaryDiv anyPosWidth (forcePos BV.srem)
+  , testProperty "sdiv" $ wfBinaryDiv anyPosWidth (forcePos BV.sdiv)
+  , testProperty "smod" $ wfBinaryDiv anyPosWidth (forcePos BV.smod)
+  , testProperty "abs" $ wfUnary anyPosWidth (forcePos BV.abs)
+  , testProperty "negate" $ wfUnary anyWidth BV.negate
+  , testProperty "signBit" $ wfUnary anyPosWidth (forcePos BV.signBit)
+  , testProperty "signum" $ wfUnary anyPosWidth (forcePos BV.signum)
+  , testProperty "umin" $ wfBinary anyWidth (const BV.umin)
+  , testProperty "umax" $ wfBinary anyWidth (const BV.umax)
+  , testProperty "smin" $ wfBinary anyPosWidth (forcePos BV.smin)
+  , testProperty "smax" $ wfBinary anyPosWidth (forcePos BV.smax)
+  , testProperty "concat" $ property $ do
+      Some w <- forAll anyWidth
+      Some w' <- forAll anyWidth
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+      bv' <- BV.mkBV w' <$> forAll (unsigned w')
+
+      let BV.BV x = BV.concat w w' bv bv'
+      checkBounds x (w `addNat` w')
+  , testProperty "select" $ property $ do
+      Some w <- forAll anyWidth
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+      NatReprLte ix <- forAll (natReprLte w)
+      Just LeqProof <- return $ ix `testLeq` w
+      NatReprLte w' <- forAll (natReprLte (w `subNat` ix))
+      Just LeqProof <- return $ (ix `addNat` w') `testLeq` w
+
+      let BV.BV x = BV.select ix w' bv
+      checkBounds x w'
+  , testProperty "select'" $ property $ do
+      Some w <- forAll anyWidth
+      Some w' <- forAll anyWidth
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+      n <- forAll $ Gen.integral $ Range.linear 0 (2 * natValue w)
+
+      let BV.BV x = BV.select' n w' bv
+      checkBounds x w'
+  , testProperty "zext" $ property $ do
+      Some w' <- forAll anyPosWidth
+      NatReprLt w <- forAll (natReprLt w')
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+
+      let BV.BV x = BV.zext w' bv
+      checkBounds x w'
+  , testProperty "sext" $ property $ do
+      Some w' <- forAll anyWidthGT1
+      NatReprPosLt w <- forAll (natReprPosLt w')
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+
+      let BV.BV x = BV.sext w w' bv
+      checkBounds x w'
+  , testProperty "trunc" $ property $ do
+      Some w <- forAll anyPosWidth
+      NatReprLt w' <- forAll (natReprLt w)
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+
+      let BV.BV x = BV.trunc w' bv
+      checkBounds x w'
+  , testProperty "trunc'" $ property $ do
+      Some w <- forAll anyWidth
+      Some w' <- forAll anyWidth
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+
+      let BV.BV x = BV.trunc' w' bv
+      checkBounds x w'
+  , testProperty "mulWide" $ property $ do
+      Some w <- forAll anyWidth
+      Some w' <- forAll anyWidth
+      bv <- BV.mkBV w <$> forAll (unsigned w)
+      bv' <- BV.mkBV w' <$> forAll (unsigned w')
+
+      let BV.BV x = BV.mulWide w w' bv bv'
+      checkBounds x (w `addNat` w')
+    , testProperty "succUnsigned" $ wfUnaryMaybe anyWidth BV.succUnsigned
+    , testProperty "succSigned" $ wfUnaryMaybe anyPosWidth (forcePos BV.succUnsigned)
+    , testProperty "predUnsigned" $ wfUnaryMaybe anyWidth BV.predUnsigned
+    , testProperty "predSigned" $ wfUnaryMaybe anyPosWidth (forcePos BV.predUnsigned)
+    ]
+
 tests :: TestTree
 tests = testGroup "bv-sized tests"
   [ arithHomTests
   , bitwiseHomTests
   , serdeTests
   , deserTests
+  , wellFormedTests
   ]
 
 main :: IO ()