TLA+ is intentionally made to look different from a typical programming language because it is very different. Even a simple programming language is far more co

TLA+ is intentionally made to look different from a typical programming language because it is very different. Even a simple programming language is far more complex than the simple mathematics underlying TLA+. If all you want to do is to verify some simple assertion about a relatively simple program, then SPIN might indeed suit you better (assuming you can express what you want in SPIN). But TLA+'s main contribution is to allow you to design and deeply understand a complex system, and how and why it works, by reducing it to its bare essentials, and describing it at whatever level of detail you're interested in (often in multiple levels of detail, which are then formally related to one another).