Viewing profile — igornotarobot

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 go…

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 m…

> 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 simil…

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 p…

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 ne…

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 co…

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 an…

> 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…

> 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 o…

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:…

Producing positive and negative examples is exactly where model checkers shine. I always write "falsy" invariants to produce examples of the specification reaching interesting cont…

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, th…

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 …

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…

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.archiv…

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-l…

> 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 the…

> 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 r…

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 eno…

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…