igornotarobot

This is why security reports have the impact section. Every piece of software has an endless stream of bugs, but only a few of them have real effect on the users. It was pretty clear in Web3 contests. Now we see something similar on a much larger scale in all other software.

You can write everything in Lean and generate an implementation. Given that LLMs can now generate Lean proofs, this does not seem to be prohibitively expensive anymore. The real issue with distributed algorithms is that they are hard to reason about, and reasoning about them at the code level does not make the verification problem easier, it makes it harder.

The original departure time stays the same, and the delay is written separately. The same applies to trains. Well, this is how it usually works in Europe, not sure about other places.

Of course, they have flight numbers, though the destination and the departure time was a good heuristic until it was not. I am much better at remembering the departure time than an arbitrary sequence of letters and numbers.

How about two different planes departing to exactly the same destination at exactly the same time from two different terminals? That's how I missed my plane from Belgrade to Vienna. I have no other explanation but that they do it on purpose.

If the LaTeX-like syntax worries you, several projects aimed at providing PL-like syntaxes for TLA+. They vary by their degree of how much of the logic they throw away. I am not going to advertise these projects here, but you would find them on GitHub search by typing the tags like "#tlaplus #language", "#tlaplus #library", and "#tlaplus #pluscal".

I have fixed the target data structures and also make Claude compare the generated code against a python reference via PBT. However, the vibe-coded code generator stumbles upon a missed clone/copy case every now and then. This is where I am less certain that it converges.

> I run into bugs all the time so it’s probably not ready for anyone other than me to use, but I’ve managed to go pretty deep (if not wide) in just a few days of work.

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.

Litex is probably closer to TLA+ than to Lean. Both draw inspiration from untyped set theory and LaTeX.

> Just friendly remember that Open access publishing is the new business model that is more lucrative for publishing industry and it is basically a tax on research activities but paid to private entities and mostly paid by taxpayer money...

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.

It probably will, but not the way we all imagine. What we see now is an attempt to recycle the interactive provers that took decades to develop. Writing code, experimenting with new ideas and getting feedback has always been a very slow process in academia. Getting accepted at a top peer-reviewed conference takes months and even years. The essential knowledge is hidden inside big corps that only promote their "products" and rarely give the knowledge back.

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.

Afaik, formal verification worked well for hardware because most of the things in hardware were deterministic and could be captured precisely. Most of the software these days is concurrent and distributed. Does the LLM + RL approach work for concurrent and distributed code? We barely know how to do systematic simulation there.

This sounds amazing! What kind of systems take you a few hours to a few days now? Just curious whether it works in a niche (like sequential code), or does it work for concurrent and distributed systems as well?

> TLA+ is not a silver bullet, and like all temporal logic, has constraints. > > You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on”

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.

> TLA+ can specify anything that could be specified in mathematics.

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.