Finally learning TLA+ by plugging a very simplified multithreaded Java simulation of an old project's distributed, (hopefully) eventually-consistent algorithm into LLMs and asking for translations.

I'd previously tried to learn TLA+ a few times but always eventually lost interest and gave up. This approach was quick and easy. Disappointed that TLC can't really exhaustively check more than 8 steps; being O(n!), 9 steps would take months, even after all the symmetry optimizations. Maybe will look at TLAPS next.