Is the plan to build a new separation logic framework, or use e.g. iris-lean or splean as a base?

And even if fuel isn’t exposed in the program logic, I’d imagine you’d still want step indexing to allow reasoning around cyclic heap structures. My experience with getting Claude (even fable) to do step indexed logical relations/SL proofs autonomously is that it struggles hard even on toy examples, particularly around the index shuffling. Do you have a setup in mind that can scale to larger programs?

Fun project in any case! I look forward to seeing how it develops :)