Very broadly: model checkers (which most TLA+ users use) verify systems by induction, by enumerating possible states a system can take on, and showing that the

Very broadly: model checkers (which most TLA+ users use) verify systems by induction, by enumerating possible states a system can take on, and showing that the none of the states violate the system requirements. In comparison, proof assistants take a deductive approach, requiring you to show - step by step - how the requirements are satisfied by the definition of the system. Dependently typed languages move some of that burden to the type system.