IME PBT is complementary to assertions: PBT probes the space of inputs and your assertions find inputs that make your code violate invariants.

When I was writing a nontrivial data structure library I was amazed (and humbled) by how many bugs were caught by PBT (again, combined with copious assertions) but not by my unit tests (which tried to cover all the "obvious" edge cases).