Apparently it takes around 1 V100 GPU hour per proof. Wonder if something like this might make it into developer tooling eventually. Writing down some nontrivi

Apparently it takes around 1 V100 GPU hour per proof. Wonder if something like this might make it into developer tooling eventually. Writing down some nontrivial invariant like 'no deadlocks are possible' and getting the result some time later seems like it could be useful. In program verification 99% of proofs can be quickly (and decidably) be dispatched with an smt solver, the last 1% is probably quantifier instantiation which a language modle might tackle.