It is notable that TLA+ is the most frequently used notation/method on the front page, followed by Alloy. It seems this has been the case for several (many?) years. Both notations/methods were invented in the 1990s, both were influenced by Z notation (used in the 1980s and 90s) and now have completely replaced it.