Verification projects on industrial code have required reasoning about functional programming constructs in Java 8. In our experience so far, verification of functional programming in practice has needed only simple techniques such as inlining. However, in general functional programming will require reasoning about how the specifications of function objects that are inputs to a method combine to produce output function objects. This paper describes our in-progress experience in adapting prior work (Kassios & Müller) to Java 8, JML, and OpenJML.