SoroProve

⊨SOROPROVE

Contract

Vibe budget s

Would go in

Set a theorem's proof to vibe and press “Check in Lean”: a Claude agent searches for a proof or a counterexample within the budget, and every version it writes is checked by Lean here, live.

question storage value who · argument · entry point

Drop a contract .wasm to model it

Modelling

Import Lean

Paste theorem statements (the part before := is enough), for example swap_pays_out : contract ⊨ (changesBy BalanceA[caller] out).given (calls "swap" ∧ₛ buysA)