Established: March 14, 2016


IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness. It also provides a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.

IVy is joint work with the following people:

  • Oded Padon, Tel Aviv University
  • Aurojit Panda, UC Berkeley
  • Mooly Sagiv, Tel Aviv University
  • Sharon Shoham, Academic College of Tel Aviv Yaffo

IVy is an open source project hosted by GitHub.

There is an introduction to Ivy including a VM.