I've seen plenty of people use TLA+ to understand systems better without writing refinements. I also think you're in a good position to show comparative models

I've seen plenty of people use TLA+ to understand systems better without writing refinements. I also think you're in a good position to show comparative models between TLA+ and Spin or NuSMV, to show that the other two are more than adequate if you're not using refinement. I know Zave tried to do a Spin vs Alloy comparison and found Spin really frustrating.