TLA+/Context

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