TLA+ es un lenguaje de especificación formal. En otras palabras, se trata de un lenguaje de alto nivel que permite modelar algoritmos y sistemas, para posteriormente verificar programáticamente la ausencia de errores en dichos modelos.
Acabo de publicar mi primera especificación en dicho lenguaje, que podéis encontrar en https://github.com/jesmg/TLAplus-hospital.
En https://www.jesusmg.org/tla/2019/07/08/primera-especificacion-TLAplus.html he dejado un poco más de información.
¿Alguien más ha trasteado con TLA+?
Si hay interés en el tema, se puede planear una visita a Almería para hacer un taller 