[pjmlp]

From my point of view, they cannot even prove that, because in most cases there is no validation if the TLA+ model actually maps to the e.g. C code that was written.

I only believe in formal methods where we always have a machine validated way from model to implementation.

[pdhborges]

Well Coq has program extraction built in.

[Ericson2314]

Yeah and that's why it's way better than the likes of TLA+.

[ted_dunning]

See Dafny

[pjmlp]

I know it, :)

[jgalt212]

preach