Ivy and GoIvy: very fast formal verification using decidable logic in Z3

[Jason E. Aten]

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