Start with property-based testing, that'll help you learn how to specify properties without the overhead of TLA+.