TLA+ is a high-level language for modeling programs and systems.
NOTE: The official name of the language is TLA+, with the + a superscript.
It was created by Leslie Lamport and is backed by Amazon Web Services, Microsoft, and Oracle.
An extension that adds support for the TLA+ formal specification language to VS Code can be found on this website.
For more information about the TLA+ Foundation, please visit https://foundation.tlapl.us.
You can see an intro video with this programming language at https://lamport.azurewebsites.net/video/intro.html.