2 ms·

> It should be noted dafny and Verdi are better here. The problem is that the scale and complexity of systems that are verifiable by Dafny and Verdi, or dozens

by pron 6y ago

> It should be noted dafny and Verdi are better here. The problem is that the scale and complexity of systems that are verifiable by Dafny and Verdi, or dozens of not hundreds of other code-level tools, is drastically smaller than those specifiable by TLA+. You are very limited in the scale of the systems you write and verify, and so those tools are much more limited in applicability. It is true that if your program is very small and/or the properties you wish to prove are simple or very specific, then there are tools that can handle them at the code level, and that might be more convenient than TLA+ in those very specific circumstances. Also, Verdi and Dafny are research tools; TLA+ is used in the field by ordinary engineers at Amazon, Microsoft, Oracle, MongoDB and a growing number of other companies to help write software you use quite a lot (most AWS services, for example). > However there appears to be a philosophical difference: tla+ finds counter examples to the spec. Absence up to the number of states checked shows the code is bug free. Dafny, Verdi seem to proceed by showing the spec is proved through various proof checking (semi) automation. As such they don't explore state. That's not the philosophical difference, just a difference in available tooling. Both TLA+ and Dafny are just languages. Both have proof tools that employ SMT solvers for deductive proofs. TLA+ also has a model checker, and perhaps so could Dafny. The philosophical difference is that Dafny is a code-level tool, and so gives you "full cover" but only in limited circumstances, while TLA+ gives you a more partial cover but in a much wider range of use-cases. > But if you tell the same team we'll be using formal methods there's a lot of complaining because FM can't check everything ... Not down to the real final code ... So why bother? I find this dichotomy disingenuous by programmers. I don't know if I'd use the word disingenuous. I think it's just unfamiliarity. The goal of FM tools aimed at "ordinary" software is not to produce perfect software but to eliminate more bugs more cheaply than with tests alone. They shouldn't be compared to a hypothetical perfection, but to what developers use now.

doonesbury 6y ago
>I don't know if I'd use the word disingenuous. Point taken. Programmers may see project uncertainly as less pressing/difficult while formal methods are onerous. How much one or the other depends on details, and how the team frames risk and methods to reduce it. Even on the project side, for example, the Chaos report from the 1990s shows some 40% (60% at small companies) of software projects are cancelled before delivering anything mainly due to scope change and lack of executive support. Both require attention. Both are non-trivial. While we're on formal methods I'd like to solicit your opinion a bit more. I am working on a distributed KV store which I'd like to formally certify. I started with TLA+ except that compared to Dafny, Verdi the gap between spec and implementation is higher. I don't like that. Verdi, in particular, comes with formally verified, shimmable network layers plus the ability to produce runnable code from the Coq spec. My practical assessment is, + Dafny: pros: Refine spec to implementation; provides safety and liveness checks. Can produce runnable code towards testing, Q/A experimentation. - Dafny: cons: The Dafny GIT repo is a mess --- extremely disorganized and therefore hard to simulate examples in papers with the real thing. It's very hard to see what libraries to build on. + Verdi: pros: Like Dafy which came after Verdi, it's focused on refinement: go from spec to more and more implementation detail. It's based on Coq proofs and Coq has tons of books, examples, exercises. See https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ for five solid write-ups concluding with formally certified C code. So I do not see Verdi as overly academic. It has formally verified libraries that can be re-used esp. in the area of message passing, marshalling which models reliable and non-reliable packet delivery. Moreover, and this is important for distributed programming, proofs can be done in terms of traces. Not sure if TLA+ and it's model checker TLC can do that. - Verdi: Cons: I have to learn Coq, not the end of the world but it's another chunk of work. Also Verdi can't help with liveness checks while TLA+ and Dafny or Spin can. I initially worked with SPIN and TLA+: those specs are checked in a model checker which looks for counter examples. I have a certain feel for that. On the other hand as I understand it out the box, Dafny or Verdi or FRAMA-C use proofs. Now a proof is formal and is help, however, I am unclear if Dafny, or Verdi will give me a counter example if a refinement goes wrong. More specifically, if a refinement is wrong which happens: one is unable to prove a claim - and that's your head's up ... or at some point a run of the executables made will assert a violation of a safety property. I'm not sure. + TLA is of course much used in industry -- so I won't plough that field again. But I wish I knew if it can prove system properties through traces like Verdi because it seems such a natural way to reason about distributed systems. TLA+ of course does liveness and safety checks. All of these are free tools ... including SPIN ... so if one can put the time in you can get a lot of power. That's good to know. Navigating some of the finer details as I suggest here is not so easy when choosing one. For my little project I was thinking Verdi for safety and TLA+ for liveness checks when needed. Please weight in ... I'd love to hear more perspectives.
- doonesbury 6y ago
  I want to better motivate my question on traces by quoting from a paper I enjoyed reading: https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-pldi15.pdf https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-... which gives this example for a distributed lock: mutex(τ ) := τ = τ1 ++ (n1, Grant) ++ τ2 ++ (n2, Grant) ++ τ3 → (n1, Unlock) ∈ τ2 What this safety requirement means is that if the lock is granted in some pending message to host n2 (say delivered or in queue to be delivered) then it must have been proceeded by an unlock message and not on the same host getting the grant --- in fact on the last node who was granted the lock. Here n1, n2 designate hostIds. What I like about this approach, is that Verdi seems to make it quite easy to model and specify in terms of nodes, processes on nodes, and messages between nodes whether on a reliable or non-reliable network. And safety conditions seem to naturally flow, in part, from how messages are ordered when sent. Of course, in an unreliable network which Verdi can model too, they may come out of order requiring more work to de-dup and/or ensure exactly-once-delivery.
- pron 6y ago
  You might be overthinking this. What you want is a cost-effective way of reaching the correctness you need; i.e. a good bug-found-per-hour rate. Unless you have a lot (years) of experience writing formal proofs, I suggest you try them, first. They generally do not have a good correctness ROI compared to other methods. But nothing and no one can give you an answer without knowing the particulars of your project, the people working on it, and the correctness goals. You'll have to try a few things for a bit and then make up your mind. Just remember that 1. the smaller your project is and the fewer people working on it the less the particular formal method chosen matters, and 2. in formal methods, going from 99.999% correct to 99.9999999% correct can be a 10x factor in cost, so the assumption that more correct = better is generally wrong as there are diminishing returns. Of course, if you just want to do this to learn about formal methods rather than find one that you can frequently use in large projects, then the choice matters even less. In terms of basic principles, the tools you mentioned are much closer to one another than they are different.

by pron 6y ago

doonesbury 6y ago

>I don't know if I'd use the word disingenuous. Point taken. Programmers may see project uncertainly as less pressing/difficult while formal methods are onerous. How much one or the other depends on details, and how the team frames risk and methods to reduce it. Even on the project side, for example, the Chaos report from the 1990s shows some 40% (60% at small companies) of software projects are cancelled before delivering anything mainly due to scope change and lack of executive support. Both require attention. Both are non-trivial. While we're on formal methods I'd like to solicit your opinion a bit more. I am working on a distributed KV store which I'd like to formally certify. I started with TLA+ except that compared to Dafny, Verdi the gap between spec and implementation is higher. I don't like that. Verdi, in particular, comes with formally verified, shimmable network layers plus the ability to produce runnable code from the Coq spec. My practical assessment is, + Dafny: pros: Refine spec to implementation; provides safety and liveness checks. Can produce runnable code towards testing, Q/A experimentation. - Dafny: cons: The Dafny GIT repo is a mess --- extremely disorganized and therefore hard to simulate examples in papers with the real thing. It's very hard to see what libraries to build on. + Verdi: pros: Like Dafy which came after Verdi, it's focused on refinement: go from spec to more and more implementation detail. It's based on Coq proofs and Coq has tons of books, examples, exercises. See https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ for five solid write-ups concluding with formally certified C code. So I do not see Verdi as overly academic. It has formally verified libraries that can be re-used esp. in the area of message passing, marshalling which models reliable and non-reliable packet delivery. Moreover, and this is important for distributed programming, proofs can be done in terms of traces. Not sure if TLA+ and it's model checker TLC can do that. - Verdi: Cons: I have to learn Coq, not the end of the world but it's another chunk of work. Also Verdi can't help with liveness checks while TLA+ and Dafny or Spin can. I initially worked with SPIN and TLA+: those specs are checked in a model checker which looks for counter examples. I have a certain feel for that. On the other hand as I understand it out the box, Dafny or Verdi or FRAMA-C use proofs. Now a proof is formal and is help, however, I am unclear if Dafny, or Verdi will give me a counter example if a refinement goes wrong. More specifically, if a refinement is wrong which happens: one is unable to prove a claim - and that's your head's up ... or at some point a run of the executables made will assert a violation of a safety property. I'm not sure. + TLA is of course much used in industry -- so I won't plough that field again. But I wish I knew if it can prove system properties through traces like Verdi because it seems such a natural way to reason about distributed systems. TLA+ of course does liveness and safety checks. All of these are free tools ... including SPIN ... so if one can put the time in you can get a lot of power. That's good to know. Navigating some of the finer details as I suggest here is not so easy when choosing one. For my little project I was thinking Verdi for safety and TLA+ for liveness checks when needed. Please weight in ... I'd love to hear more perspectives.

doonesbury 6y ago
I want to better motivate my question on traces by quoting from a paper I enjoyed reading: https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-pldi15.pdf https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-... which gives this example for a distributed lock: mutex(τ ) := τ = τ1 ++ (n1, Grant) ++ τ2 ++ (n2, Grant) ++ τ3 → (n1, Unlock) ∈ τ2 What this safety requirement means is that if the lock is granted in some pending message to host n2 (say delivered or in queue to be delivered) then it must have been proceeded by an unlock message and not on the same host getting the grant --- in fact on the last node who was granted the lock. Here n1, n2 designate hostIds. What I like about this approach, is that Verdi seems to make it quite easy to model and specify in terms of nodes, processes on nodes, and messages between nodes whether on a reliable or non-reliable network. And safety conditions seem to naturally flow, in part, from how messages are ordered when sent. Of course, in an unreliable network which Verdi can model too, they may come out of order requiring more work to de-dup and/or ensure exactly-once-delivery.
pron 6y ago
You might be overthinking this. What you want is a cost-effective way of reaching the correctness you need; i.e. a good bug-found-per-hour rate. Unless you have a lot (years) of experience writing formal proofs, I suggest you try them, first. They generally do not have a good correctness ROI compared to other methods. But nothing and no one can give you an answer without knowing the particulars of your project, the people working on it, and the correctness goals. You'll have to try a few things for a bit and then make up your mind. Just remember that 1. the smaller your project is and the fewer people working on it the less the particular formal method chosen matters, and 2. in formal methods, going from 99.999% correct to 99.9999999% correct can be a 10x factor in cost, so the assumption that more correct = better is generally wrong as there are diminishing returns. Of course, if you just want to do this to learn about formal methods rather than find one that you can frequently use in large projects, then the choice matters even less. In terms of basic principles, the tools you mentioned are much closer to one another than they are different.