I think the use of TLA+ is very niche, just to prove that some really lower level algorithms for distributed systems work well, I think crypto might be a good use case like you mentioned, but I guess most companies wouldn’t benefit from it except if for fun