Burnt Sushi only uses the type to generate values. Proptest lets you constrain the values more precisely. Eg you can create a btreemap with up to 5 entries where the keys are some subset of ints (say) and the values are some subset of some other type. This can capture many of the constraints of a functions precondition and can be implemented efficiently in both fuzzers and verifiers.