I have a dilemma, ROCQ or TLA+

[Neil Talap]

Hi, I am Neil.

I have a dilemma: to just focus on a formally verified design but not a formally verified implementation while using TLA+.

OR

Full formal verification of the design and of the implementation with ROCQ.

I genuinely like the simplicity and the set theory approach that the TLA+ uses. I have enjoyed working and thinking in terms of state machines, it has been great.

But ROCQ is also genuinely attractive, even though it uses type theory. 

ROCQ and TLA+ are attractive, I tried to combine the two, but they use fundamentally incompatible philosophies. You cannot do two at the same time and benefit from it. It will result in wasted effort and time.

Does anyone have a better understanding of this?

[Stephan Merz]

Hi Neil,

having to decide between two different techniques for formal verification may be seen as a luxury.

In my experience, TLA+ is most useful when reasoning at the algorithmic level. At this point in time, to my knowledge there is no formally verified pathway from a TLA+ specification to a correct executable implementation. This being said, LLMs appear to become capable of generating code from TLA+ specs, and there are techniques such as trace validation for checking implementations against TLA+ specs – even if they do not give you as strong correctness guarantees as a formal proof, they are very effective for catching bugs.

Frameworks such as Verdi [1] (implemented in Rocq) have been designed to formally prove distributed systems, going all the way from algorithms to executable code, and they have impressive results. I would expect such a framework to require more proof effort because you have to reason at a lower level of abstraction than your typical TLA+ spec. Another potential drawback is that you are limited to the programming primitives that the framework provides, unless you are prepared to extend it.

My 2 cents,

Stephan

[1] https://github.com/uwplse/verdi

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/616d53a6-48f4-4d54-b4df-a78fcd776d65n%40googlegroups.com.