Finding a language that is $NP^L$-complete

I'm trying to prove a theorem and as a lemma I would like to identify an $NP^L$-complete language. I was thinking something like a machine that can decide $SAT$ equipped with an oracle for $L$ can decide every language in $NP^L$, but I'm not sure how to formalize this. Here's my attempt at doing so

$$ SAT^L = \{\text{satisfiable boolean formulas with some clauses as }L(x_1, \dots, x_k)\}$$

The clauses that are of the form $L(x_1, \dots, x_k)$ are queries that are true if and only if $(x_1 \cdots x_k) \in L$.

I think $SAT^L$ is $NP^L$-complete, for any language $L$, but I don't know how to prove this. It's of course in $NP^L$ since we can take a witness
assignment and check it, and we can check the $L(\cdot)$ predicates with a query to our oracle to $L$. I'm not sure how to prove $NP$-hardness though.

I was thinking of just modifying Cook-Levin's construction so that I could add additional clauses to the formula of the form $L(x_1, \dots, x_k)$ when encoding the computation graph of an NTM $M^L$ but I'm not sure if this works in general, and is honestly more of a rough idea than anything else. This construction seems to be pretty sensitive to the "implementation" of the oracle queries, so I'm not sure how to make this rigorous.

Is there a more standard example of a $NP^L$-complete language?

What you are looking for is a relativization of the Cook-Levin theorem in the sense that you consider SAT and NP relative to an oracle for $L$. You can find the answer to that in this answer, point number 2. There you get (an extension of) Circuit-SAT as a complete language; reducing this to your version of SAT should not be too hard.

Note that, as mentioned in the linked answer, this is a bit different than a relativization in the sense that it is the reduction which possesses an oracle for $L$.

StackExchange Computer Science Q#109321, answer score: 2