We propose to add a new, optional syntactic construct to postcondition assertions, called *postcondition* captures. Postcondition captures are spelled in the same fashion as lambda captures. They are placed immediately after the `post` contextual keyword and before the predicate: `post [``captures``] (``predicate``)` Postcondition captures are variables constructed when the function is called. They are visible only to the predicate of the postcondition assertion they are associated with. With a