Markus A. Kuppe: Teaching TLA+ to Engineers at Microsoft. FMTea 2023: 66-81