TLA+/Context

• To analyze a system correctly before it is implemented, a language to model the system and automatic tools to prove the system is required.
• Mathematics is more expressive to model system and independent of the order of execution.