Post

Just tried to run my "benchmark" proof (PCF+ref type preservation) on Fable 5. It took 10 minutes and did not make ONE SINGLE ERROR. No tactics out of place, no iteration. Just full Rocq proofs the first time. This is mental.

10/6/26, 8:24 pm0 reposts1 like

River 🏳️‍🌈 ❤️

@riverofberlin.bsky.social

10 June

yeah but this also costs more than an SWE lol, this model is amazing and financially unusable after the trial window ends imo

gavin.codes

@gavin.codes

11 June

Only 60% more expensive than deepseek for my proofs, and twice as fast. The token efficiency almost makes up for the cost.