LLMs can write TLA+ models just fine. It can help even with small mobile apps. Surprisingly, simple TLA models were able to find design/workflow issues almost in every of a few vibe-coded apps I've tried on vacation.