Not really a professional setting, but I teach TLA+ to the above average kids in my class (I teach 2 hours a week) in high school (15 / 16 yo). I started this a few weeks ago as an experiment, but the results are great. The students are enthousiastic, and while they need a bit of help, it's not too hard to get into for simpeler projects. So far a student has used it to model his rubiks cube solving bot can do every move a human can. Furthermore, we are currently using it for proving their anti collision system for multiple robots navigating a grid is sound.