@regehr@mastodon.social @whitequark@mastodon.social @lenary@types.pl @unlambda@hachyderm.io As an alternative, although we also use CVC5/Z3 directly in our compiler verification efforts, I've always wanted to move towards using a verification IL like Why3 instead of directly using a SMT solver. Boogie used to be very popular, and I think it's being developed again, and I've always felt you could save time with a verification language.