Auctions are used to sell goods worth trillions of dollars annually.
Many of them are well established, frequently used, and hence well tested.
However, in some domains new auction schemes are developed and only infrequently used. These can benefit most from formal methods.
We report here how verified code can be extracted using Isabelle's extraction mechanism for so-called dynamic auctions, that is, auctions in which participants can bid in several rounds.
We use co-recursion in order to reason about and extract code for dynamic auctions in which inputs and computations are interleaved.