They describe it later. Essentially, they are asking the AI for each function to give them a property that basically means "this function is correct", and then they let it prove that property.