yeah I am looking as well - I have an application that lets you specify state based behaviour for industrial automation and functional safety as an executable specification, and part of this is once the specification is data then formal methods translation looks do-able
So I am already generating functionality in a few different languages of code for export OK, but not TLA+ yet
Currently I end up in negotiations with a prospective buyer, so maybe I won't get there first, but if there was a starting point of a codebase or similar I could leverage off, that would be great.