IVy is a research tool 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. 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.
Hello, ivy on the Python 3 branches (both 2to3new and qpdr) gives strange results compared to master. For example, ivy_check trace=true token.ivy prints a trace with obvious contradictions (e.g. env.has_started(0) = true env.has_started(0) = false) while the master version prints a different, more sensible trace. token.ivy is here: https://github.com/dranov/soroban-decidable-verification/tree/a304495e47f248ac991cc4814f1f2a4040139987/models
Hello, ivy on the Python 3 branches (both
2to3newandqpdr) gives strange results compared tomaster. For example,ivy_check trace=true token.ivyprints a trace with obvious contradictions (e.g.env.has_started(0) = true env.has_started(0) = false) while themasterversion prints a different, more sensible trace.token.ivyis here: https://github.com/dranov/soroban-decidable-verification/tree/a304495e47f248ac991cc4814f1f2a4040139987/models