Finding a good loop invariant
You have an intended postcondition for a loop, and you're looking for an interesting invariant. In this scenario, try taking the intended postcondition, and replacing the total number of iterations (here N) by the number of iterations so far (here i). There's no guarantee that this is an invariant: that's only the case if the way the postcondition is somehow related to the structure of the loop. But if it is an invariant, it's definitely interesting, because it lets you prove the postcondition.

So we're interested in the following property: “the value of found equals the value of the predicate there exists a $k$ in the range $[0, i)$ such that $a[k] = x$”. Note that I use a name other than i for the existential variable, since i is now used in the context. The quantifier pile-up is:
for any value of N set before calling this snippet,
for any value of the variable i,
there exists an index $k$ such that …

It is easy to verify that this is indeed an invariant of the loop.

Intuitively, this property states that found reflects whether the element is in the array up to the point that has been traversed. At the end of the loop that traverses the whole array, found reflects whether the element is in the whole array.