Having similar experience with my experimental code generator to Rust. Every time a yet another example does not work, Claude fixes it. However, I am curious whether it would converge to a bullet-proof solution, or I have to carefully read the code and come up with proper abstractions.

While I do not disagree with this statement, this makes a significant difference for the citizens who do not happen to work in academia. Before open access, the journals would try to charge me $30-50 per article, which is ridiculous, it's a price of a textbook. Since my taxes fund public research in any case, I would prefer to be able to read the papers.

I would also love to be able to watch the talks at academic conferences, which are, to very large extent, paid by the authors, too.

LLMs enable code bootstrapping and experimentation faster not only for the vibe coders, but also for the researchers, many of them are not really good coders, btw. It may well be that we will see new wild verification tools soon that come as a result of quick iteration with LLMs.

For example, I recently wrote an experimental distributed bug finder for TLA+ with Claude in about three weeks. A couple of years ago that effort would require three months and a team of three people.

I think people get confused by the word "temporal" in the name of TLA+. Yes, it has temporal operators. If you throw them away, TLA+ (minus the temporal operators) would be still extremely useful for specifying the behavior of concurrent and distributed systems. I have been using TLA+ for writing specifications of distributed algorithms (e.g., distributed consensus) and checking them for about 6 years now. The question of liveness comes the last, and even then, the standard temporal logics are barely suitable for expressing liveness under partial synchrony. The value of temporal properties in TLA+ is overrated.

You are talking about the logic of TLA+, that is, its mathematical definition. No tool for TLA+ can handle all of mathematics at the moment. The language was designed for specifying systems, not all of mathematics.

- TLAPS is the interactive proof system that can automate some proof steps by delegating to SMT solvers: https://proofs.tlapl.us/doc/web/content/Home.html

- Apalache is the symbolic model checker that delegates verification to Z3. It can prove properties without executing anything, or rather, executing specs symbolically. For instance, it can do proofs via inductive invariants but only for bounded data structures and unbounded integers. https://apalache-mc.org/

- Finally, TLC is an enumerative model checker and simulator. It simply produces states and enumerates them. So it terminates only if the specification produces a finite number of states. It may sound like executing your specification, but it is a bit smarter, e.g., when checking invariants it will never visit the same state twice. This gives TLC the ability to reason about infinite executions. Confusingly, TLC does not have its own page, as it was the first working tool for TLA+. Many people believe that TLA+ is TLC: https://github.com/tlaplus/tlaplus

Having a specification does not mean that one should not touch it. It is just a different level of experimental thinking.

However, there are no model checkers for Lean. Currently, you either have to write a full proof by hand, with some assistance from LLMs, or rely on random simulation, similar to property-based testing.

[1] https://protocols-made-fun.com/lean/2025/04/25/lean-two-phas... [2] https://protocols-made-fun.com/lean/2025/05/10/lean-two-phas...

- Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan...

- Coral: https://www.microsoft.com/en-us/research/project/q-program-v...

- Ivy: https://github.com/microsoft/ivy

This is interesting, because undecidability of SMT theories is a very practical issue. Actually, many people in academia have this point of view that solving many practical problems is useful. It helps us to drive research progress, but it is a completely useless metric for industry. What is better: (1) a tool that wins a competition by solving X out of Y benchmarks, (2) or a tool that solves your problem? In academia, (1) is a clear winner, as it gives you a free way to publish a paper, modulo peer review. In industry, you don't care about (1), because you have exactly 1 (one!) benchmark that is important for you, that is, case (2).

Imagine a compiler that works on 85% of syntactically-correct (and well-typed) programs, and you never know when it would hang on your code. This is exactly the behavior of SMT solvers when you start using quantifiers. By knowing the internals of SMT and its techniques, you can quite often work around these problems. However, TLA+ users do not want to know the guts of SMT; why would they? This is why Apalache implements a quantifier-free encoding. Sometimes, it hits us badly, but it is somewhat more predictable. Ivy does it differently, by providing the user with a language that is actually quite close to the theories implemented in z3. While it gives the user a finer control over the SMT constraints, the user has to understand first-order logic much better than in case of Apalache.

There are several issues regarding liveness:

1. Afaik, NuSMV implements the standard propositional encoding of lasso detection with SAT [1], which should also work SMT (when we can guarantee that the transition system is finite). While I am sure this is the case for NuSMV, it is a bit of guessing in case of nuXmv as it is available in binaries, and its default license prohibits industrial use. Although the encoding [1] is linear in the formula size, it is still producing a lot of constraints. Unfortunately, practical TLA+ specifications are very heavy on fairness constraints (WF and SF), which are actually expressed as formulas over []<>p and <>[]q. So we first have to make Apalache scale to bounded model checking of safety, before trying it in a much harder setting.

2. Apalache also supports integer constants (under some syntactic assumptions), e.g., one can write \E x \in Int: P. While this makes Apalache quite useful in reasoning about timestamps, such specifications are infinite-state. That requires generalized liveness-to-safety reductions, such as the one implemented in Ivy.

3. Finally, distributed systems quite often require non-standard liveness. For instance, it is often the case that messages should be delivered within a predefined time interval. While we can model these systems by writing LTL formulas, this usually leads to huge LTL formulas, so see point 1. Moreover, some distributed systems have only probabilistic liveness guarantees. In this setting, the benefit of LTL is less obvious than the benefit of safety checking. It may be easier and more efficient to write a liveness monitor by hand, rather than rely on an automatically generated one, which will for sure explode.

[1] Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan: Linear Encodings of Bounded LTL Model Checking. Log. Methods Comput. Sci. 2(5) (2006)

If you like to check your specification for arbitrary parameters, then you will have to use quantifiers in z3, which would require a lot of care to write SMT constraints in a way that helps z3 to deal with the quantifiers. The mix of sets and cardinalities is especially hard for SMT. Although academia is making a lot of progress in this direction, e.g., see [1], the mainstream solvers are still leaving you with the problem of encoding sets and cardinalities all by yourself.

Some provers use quantifiers in z3. For instance, IVy [1] can check inductive invariants of systems that have arbitrary size. However, you have to rewrite your specification in uninterpreted first-order logic, e.g., you would have to think about abstracting away integers. Moreover, to make invariant checking decidable, you would have to transform your specification into a special fragment that is called EPR.

[1] Ruzica Piskac. Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints. VMCAI, 2020. https://link.springer.com/chapter/10.1007%2F978-3-030-51074-...

[2] http://microsoft.github.io/ivy/