@yosh this is where I spend a lot of my ai thought right now too. Like, coming up with models that interact with correctness checks seems like the only way to go from generation to creation reliably, but the expense of every iteration going through correctness checks feels like a lot. It also seems like working on integration of one proofing/correctness approach wouldn’t really further other approaches, so the work seems huge and like it would never get easier/quicker?