В рамках проекта возникла задача использовать символьное выполнение (symbolic execution) некоторого псевдокода, получающегося из программы. Один из участников активно продвигает Z3 от микрософта, но мне эта идея категорически не нравится (проект будет открыт). Нашел много - OpenSMT, VeriT, Coq (?), etc. Но нужен совет, и еще, существует ли такая программа, но на Haskell. Жду советов и просвещения.