"IVy is a language and a tool for specifying, modeling, implementing and verifying protcols. IVy is intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. A particular focus of IVy is to provide automated proof in a way that is predictable, stable and transparent, in order to improve the overall productivity of the verification process. 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. The Ivy language is designed to be well suited for both abstract specification and efficient implementation."
Last modified 10 May 2020