This is spelled "clock_id invalid" elsewhere.

In fact all cases could benefit from providing the wrong value that triggered the EINVAL, but this is optional.

The format needs to be %ju. I.e. all format specifiers must be for (u)intmax_t. On the other hand, I do not think that the casts of the arguments to intmax are needed.

This and related bits are unrelated, right?

OK. I'm super confused about how that could possibly work. Why aren't the casts needed, and why does this have to be %ju? I missed something, somewhere I think.

oh my! Yes, that's a leakage of something else I'm working on.

The format string and the arguments are copied intact from kernel to usermode. Usermode, libc specifically, does the formatting. Arguments are marshaled through uint64_t objects, and are cast to uintmax_t for the formatting.

This is done so no memory allocation happens in kernel on error, so that EXTERROR() works in almost any context that has a valid struct thread.

It is documented in exterror(9)

Suggest being more specific:

 if (!timespecvalid_interval(ats)) {
        if (ats->tv_sec < 0)
                return (EXTERROR(EINVAL, "Backward clock jump"));
        return (EXTERROR(EINVAL, "Out of range tv_nsec %jd",
            ats->tv_nsec));
}