PV6 IVydeductively or inductively proves or helps prove program properties

Application domain/field

Type of tool

Protocol verifier

Expected input



.ivy file (program specified in the IVy language)

Expected output

Depends on the mode of operation:
  1. ivy_check checks the proof of an IVy program, will return PASS or FAIL
  2. ivy will allow the user to interactively construct inductive invariants
  3. ivy_to_cpp will result in a C++ program extracted from the IVy program


Used for specifying, modeling, implementing and verifying protocols. "Tool for correct design and implementation of distributed protocols and algorithms, supporting modular specification, implementation and proof" Some things it can do: Uses ABC, Z3.


License: MIT
Framework Model checking Protocol


Related papers

Ivy: A Multi-modal Verification Tool for Distributed Algorithms (CAV 2020)

Last publication date

14 July 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.