I've put a document at http://cr.openjdk.java.net/~briangoetz/eg-attachments/Coverage.pdf
which outlines a formal model for pattern coverage, including record patterns and the effects of sealing. This refines the work we did earlier. The document may be a bit rough so please let me know if you spot any errors. The approach here should be more amenable to specification than the previous approach.
