Introduce three ways to represent transactions: wire, ledger and for-verification.
TransactionForVerification contains the arguments formally passed to verify(). Making Contract.verify() take only a single object as the argument makes it easier to evolve the Contract binary interface without breaking backwards compatibility with existing contracts that are uploaded to the ledger. The Kotlin "with" construct can be used to bring the members into scope, thus acting syntactically like function arguments.
Make the contracts to be run depend on both input AND output states: this approach seems simpler than trying to have some notion of marking outputs that are checked. The TransactionForVerification class implements this simple logic (it's all moved into Transactions.kt).