I wonder whether there is or could be any knowledge and/or experience sharing between Cicada and Kind2 (or HVM). https://github.com/Kindelia/Kind2 https://github.com/Kindelia/HVM Thoughts?