One thing that will help drive adoption is the ability to run SMT solvers more quickly so the proof stage of your design/build has a faster feedback loop. I ra

One thing that will help drive adoption is the ability to run SMT solvers more quickly so the proof stage of your design/build has a faster feedback loop. I ran some experiments with the Z3 and alt-ergo solvers (verifying SPARK/Ada code using GNATprove) on a base M1 Mini and it absolutely screamed, I’m not normally a Mac fan-boy but new chips like the M1 Ultra might have the possibility of driving a mini-renaissance in FV. I’d like to see more attention being given to GPU accelerated SMT solvers too but haven’t seen much movement outside of a handful of research papers.