TLA+ is a formal specification language invented by Leslie Lamport, ACM Turing award winner. 

Amazon Web Service is expanding the database team using TLA+ as the formal method tools in their key projects, such as DynamoDB. 

This course introduces the fundamental knowledge of TLA+ in an incremental way. Moreover, it illustrates the methodology of formal verification using TLA+.