What is the LTL expression for "there is a value of y whose next value is 8"?
The important thing that is missing from your question is how you model your program, and specifically, what are the atomic propositions you allow.

If your atomic propositions are "y=0",...,"y=8", and your transition system is modeled accordingly, then the formula $FX y=8$ means the eventually, the next position would have "y=8". Note that this is equivalent to the formula $XF y=8$, which basically says that y=8 sometime after the first position.

However, you phrased your requirement as "there is a value of y whose next value is 8", and it's not clear what this means. What is the "next value of y"? LTL does not recognize y as an entity, only the propositions mentioned above. So you cannot really talk about values of variables in LTL, without first adding all possible values as propositions.