how to formally arrive at a correct EBNF grammar of a language
Your informal description of your language could certainly be made more precise, in the same way as you could make the description of any (mathematical) set more precise until you've written the description out in mathematical notation. In that sense, EBNF is similar to what you get when you recast an informal description of a language into a mathematical formalism. (EBNF doesn't quite qualify, but the BNF formalism which inspired EBNF is a precise formalism.)

In between the formal description of a language and the practical question of building a parser for the language, a number of practical issues need to be dealt with, many of them having to do with the way a string of characters is grouped into meaningful tokens in the concrete representation of the language. In other words, questions like "where can spaces and newline characters be placed?" "Can I insert comments into an expression?" and so on. It's possible to write these into a formal description of a language, but the end result is often not particularly useful for the casual reader because the high-level structure of the language is overwhelmed by pesky details.

I note in passing that your grammar requires that AND and NOT appear with precisely one space preceding and following, while no spaces are allowed around the &gt;= operator (and friends). That means that several of your examples don't match the EBNF. For example, time &gt;= 2020-01-09 would have to be written as time&gt;=2020-01-09 and response:success AND NOT os:windows as response:success AND  NOT os:windows (with two spaces between AND and NOT). I doubt that was your intent, and I don't say this to criticise; just to point out how tricky it can be to get the details right, so that it can actually be used to construct a concrete parser, and still make the grammar usable for human readers. The usual approach is to separately formalise the division of the text into lexemes ("tokens") and the syntactic structure of the language, which treats the inputs as a stream of tokens rather than as a stream of undifferentiated characters. That's by no means formally necessary, and a lot of the applications of EBNF do in fact attempt to be precise to the character level, but a close examination of these EBNF applications might reveal the practical limitations of this strategy.

As I said in a comment, for any language for which a context-free grammar exists, there are an unlimited number of other context-free grammars which derive the same language. However, the question of whether two context-free grammars derive the same language is undecidable; no algorithm exists which can always correctly make that determination. Consequently, it is also impossible to enumerate all the grammars which could derive a given language (however that language is given).

In addition, there are competing mathematical formalisms which could be used to describe a language. After all, a language is a set, and any mathematical expression which precisely defines a set is a possible formal language description. (Some of these will be more practically usable than others.) So there's no way to say whether a procedure exists to generate a description in one formalism from a description in another formalism without know what, exactly, the nature of the two formal systems is. Sometimes it will be possible, other times not.

If you only want to know if a given text is in a language, then any of the unknowable infinitude of possible grammars for that language will suffice, although it's better if the grammar formalism used is computationally tractable. But most of the time, you don't just want to know that a text is in a language. (A C "compiler" whose only possible output is one of the messages "yes, that is a well-formed C program" and "no, that is not a well-formed C program" is unlikely to attract many paying customers, even if its judgement is 100% correct.) In most applications, you want to parse the language in order to reveal the syntactic structure of a valid text. To do that, your grammar should reflect the syntactic structuring you have in mind, and not all of the possible grammars for the language do.