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,…
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…
> 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…
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…
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…
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…
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…
> 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…
TLA+ is just a language for writing specifications (syntax + semantics). If you want to prove anything about it, at various degrees of confidence and effort, there are three tools: - TLAPS is the interactive proof…
Producing positive and negative examples is exactly where model checkers shine. I always write "falsy" invariants to produce examples of the specification reaching interesting control states for at least one input.…
It should be possible to write protocol specifications in Lean, e.g., this is a recent case study on specifying two-phase commit in Lean [1] and proving its safety [2]. However, there are no model checkers for Lean.…
When you say peer reviews, do you mean academic publications or testimonials? I imagine it would be difficult to publish a paper at an academic conference proposing an alternative syntax for anything, even if it were…
I believe this is really the tragedy of formal verification tools. Everybody wants a tool as robust as a compiler. At the same time, nobody wants to invest into development of such tools. Microsoft Research 20 years ago…
Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/. And here…
True. There are many frontends for Z3 that focus on various domains. For instance, those developed at Microsoft: - Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan... - Coral:…
> Of course decidability is desirable, but efficient sound procedures in the undecidable case would still solve many practical problems. I realize they are not as "nice" from a theoretical/academic standpoint, though.…
> Other examples would be checking liveness properties in the unbounded case, and possibly full Linear Temporal Logic, e.g., <>[]p ("eventually, property p is always satisfied"). I realize this is a tall order, but I…
Just curious, what more complex properties do you like to be supported in Apalache? Many tools that are built on top of z3 are checking inductive invariants. By having a strong enough inductive invariant, you should be…
Yes, it is weird. Now imagine. You learn English as a foreign language at school. You do a PhD and move for a postdoc to another country, say, Austria, because that's how academics do it. You work there, though you are…
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,…
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…
> 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…
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…
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…
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…
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…
> 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…
TLA+ is just a language for writing specifications (syntax + semantics). If you want to prove anything about it, at various degrees of confidence and effort, there are three tools: - TLAPS is the interactive proof…
Producing positive and negative examples is exactly where model checkers shine. I always write "falsy" invariants to produce examples of the specification reaching interesting control states for at least one input.…
It should be possible to write protocol specifications in Lean, e.g., this is a recent case study on specifying two-phase commit in Lean [1] and proving its safety [2]. However, there are no model checkers for Lean.…
When you say peer reviews, do you mean academic publications or testimonials? I imagine it would be difficult to publish a paper at an academic conference proposing an alternative syntax for anything, even if it were…
I believe this is really the tragedy of formal verification tools. Everybody wants a tool as robust as a compiler. At the same time, nobody wants to invest into development of such tools. Microsoft Research 20 years ago…
Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/. And here…
True. There are many frontends for Z3 that focus on various domains. For instance, those developed at Microsoft: - Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan... - Coral:…
> Of course decidability is desirable, but efficient sound procedures in the undecidable case would still solve many practical problems. I realize they are not as "nice" from a theoretical/academic standpoint, though.…
> Other examples would be checking liveness properties in the unbounded case, and possibly full Linear Temporal Logic, e.g., <>[]p ("eventually, property p is always satisfied"). I realize this is a tall order, but I…
Just curious, what more complex properties do you like to be supported in Apalache? Many tools that are built on top of z3 are checking inductive invariants. By having a strong enough inductive invariant, you should be…
Yes, it is weird. Now imagine. You learn English as a foreign language at school. You do a PhD and move for a postdoc to another country, say, Austria, because that's how academics do it. You work there, though you are…