I think there's some bad nomenclature here. "Property based testing" literally means you're writing properties, which can be verified formally, or randomly (fuzzing / constrained random testing).

For example in SystemVerilog you can write properties (literally with the `property` keyword), and then they can be checked in simulation, and with formal tools.

TLA+ can do the same I believe - there are tools to verify a model randomly or formally.