# Introduction

This post contains notes from learning TLA+, a formal specification language for designing, modelling, documenting, and verifying concurrent systems.
These notes created from Practical TLA+, a book targeted towards TLA+ beginners.

TLA+ is an acronym for Temporal Logic of Actions.

## Mathematics

Human Semantics TLA+ Math
not ~ $\neg$
and /\  $\wedge$
or \/ $\vee$
in \in $\in$
notin \notin $\notin$
True T $1$
False F $0$

# Chapter 1

Use TLA+ to specify a bank wire transfer problem.

1. Each wire must occur between two different people in the bank and wire at least one dollar;
2. If the wire succeeds, value of the wire is deducted from the sender and added to the receiver;
3. If the wire fails, the two accounts are unchanged;
4. A wire may not cause an account to have a negative balance;
5. Multiple wires my occur simultaneously.