This milestone comprises the work that needs to be done for the first complete, self-contained implementation of what this draft promises: Proving soundness of combinatorial Vickrey auctions and generating verified executable code.

There are more potential improvements to be made, but the issues in this milestone are absolutely essential for the first proper paper submission derived from this draft.