Yes, you can definitely tell the inventor of TLA was also the first developer of LaTeX. As such, it is a language best read after typesetting. For a good exam

Yes, you can definitely tell the inventor of TLA was also the first developer of LaTeX. As such, it is a language best read after typesetting. For a good example, see Appendix B in Diego Ongaro's dissertation [1], the formal Raft specification. After a little of the Learn TLA+ book, I was able to muddle through the spec enough to implement it. 1: https://ramcloud.stanford.edu/~ongaro/thesis.pdf https://ramcloud.stanford.edu/~ongaro/thesis.pdf