3 ms·

It's awesome that these tools exist, but the verification codebase for Raft is 10s of thousands of lines of specification & proof files. Just installing verdi o

It's awesome that these tools exist, but the verification codebase for Raft is 10s of thousands of lines of specification & proof files. Just installing verdi on linux nearly bested me (some interaction btwn ocaml package management, coq, and native code). I tried running the verification suite and gave up after 10 or 20 minutes of full CPU. TLA has warts too -- the only way I could interact with it is via a custom java IDE. It would be great to see lighter-weight, more accessible ways to embed proofs in real-world programs and run them in test suites.

__s 9y ago
On the lightweight end there's https://github.com/catseye/Maxixe https://github.com/catseye/Maxixe
naasking 9y ago
> It would be great to see lighter-weight, more accessible ways to embed proofs in real-world programs and run them in test suites. Not sure what this means exactly. Do you mean extracting the part of the proof that can't be verified statically, for whatever reason, as some kind of test suite?
- awinter-py 9y ago
  I think I'm asking for something in between a mathematically verifiable proof and fuzzing. A lightweight way to translate runnable code into a symbolic execution environment that can be exercised (not necessarily verified) exhaustively or stochastically. There are relatively few functions that I want to do this for, and I'm okay with doing some manual work to define the possible inputs and how the functions talk to each other (i.e. mock out network / filesystem / database).
pron 9y ago
> TLA has warts too -- the only way I could interact with it is via a custom java IDE. Why? What problems did you run into with TLA+?
- awinter-py 9y ago
  couldn't figure out how to run https://github.com/ongardie/raft.tla https://github.com/ongardie/raft.tla
  - pron 9y ago
    What do you mean by "run"? Check in the TLC model checker? You need to first write a configuration that you want to check. Lamport's Specifying Systems has full documentation for using the model checker from the command line. But if you're a beginner, you might be better off using the IDE, at least at first, as it helps you write a configuration very easily. Also, I would recommend starting with a simpler specification (there are lots of examples available). Otherwise, the checker would just work for a while and spit out "OK", and won't mean much to you.
  - hwayne 9y ago
    I wrote a step-by-step tutorial to using the IDE. Hope it helps! https://learntla.com/pluscal/toolbox/ https://learntla.com/pluscal/toolbox/

__s 9y ago

On the lightweight end there's https://github.com/catseye/Maxixe https://github.com/catseye/Maxixe

naasking 9y ago

> It would be great to see lighter-weight, more accessible ways to embed proofs in real-world programs and run them in test suites. Not sure what this means exactly. Do you mean extracting the part of the proof that can't be verified statically, for whatever reason, as some kind of test suite?

awinter-py 9y ago
I think I'm asking for something in between a mathematically verifiable proof and fuzzing. A lightweight way to translate runnable code into a symbolic execution environment that can be exercised (not necessarily verified) exhaustively or stochastically. There are relatively few functions that I want to do this for, and I'm okay with doing some manual work to define the possible inputs and how the functions talk to each other (i.e. mock out network / filesystem / database).

pron 9y ago

> TLA has warts too -- the only way I could interact with it is via a custom java IDE. Why? What problems did you run into with TLA+?

awinter-py 9y ago
couldn't figure out how to run https://github.com/ongardie/raft.tla https://github.com/ongardie/raft.tla
- pron 9y ago
  What do you mean by "run"? Check in the TLC model checker? You need to first write a configuration that you want to check. Lamport's Specifying Systems has full documentation for using the model checker from the command line. But if you're a beginner, you might be better off using the IDE, at least at first, as it helps you write a configuration very easily. Also, I would recommend starting with a simpler specification (there are lots of examples available). Otherwise, the checker would just work for a while and spit out "OK", and won't mean much to you.
- hwayne 9y ago
  I wrote a step-by-step tutorial to using the IDE. Hope it helps! https://learntla.com/pluscal/toolbox/ https://learntla.com/pluscal/toolbox/