https://github.com/glycerine/ivy (and the goivy/ directory in particular).
Ivy has been used by Apple to verify hardware memory subsystem designs, and to find bugs in the QUIC spec before it was published. Executive summary: for verifying distributed systems, Ivy (and my GoIvy port, goivy_check and ivyweb) gives you not just model checking but actual full correctness proof of your system specification. And, Ivy does so very, very quickly. This is a fascinating alternative to Lean which uses un-decidable logics. For example, Ivy takes 5 seconds to check a Raft specification with goivy (my port of the original python Ivy to Go; goivy_check). With TLA+, model checking Raft can take days or weeks just for a small bounded model check -- which, even after alot of time spent brute forcing of the state space -- is still not a proof! A model check is but a check that for the small state size (e.g. 3 servers, 3 raft log entries) that you are willing to wait for. This is not particularly comforting for systems that are expected to run forever through millions of log entries, log compaction, and Raft cluster membership changes. Ivy's proofs are by induction, and so they hold for infinite state systems running for any amount of time. This is much more realistic. That is why the focus in Ivy is on interactively finding an _inductive invariant_. IVy originally stood for "Interactive Verification" -- this is what the web app (ivyweb) is for. Moreover, Ivy supports _compositional testing_. Compositional testing is critical for testing component specifications separately and then assembling them _without_ introducing new interleaving bugs. This is a great tutorial on compositional testing by Ken McMillan (Microsoft Research, UT Austin Computer Science; he invented symbolic model checking in his dissertation). He is one of the two primary authors of Ivy: https://www.youtube.com/watch?v=6WVL-Vpm5RY&t=118s The binaries ivy2cpp and ivy2go from the my ivy repo support compositional testing. >From Ivy specifications, they generate C++ and Go code that test the spec. The backend of ivy (and my ivyweb port from python to Go) uses Z3. Z3 can run either in browser (wasm) or on server (native binary). The ivyweb app shows McMillan's Ivy tutorial to let your learn by doing. The https://github.com/glycerine/ivy repo includes extensive literature citations and introductory Q & A. Video introductions to Ivy: https://www.youtube.com/watch?v=CE1mcjqea0A https://www.youtube.com/watch?v=s2Jvd_KLY20&t=397s Enjoy, Jason -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/golang-nuts/23e85ff3-cd15-44bf-8e30-4e5822cdf486n%40googlegroups.com.
