There have been a few attempts to formalize the semantics of JS, but the lambdaJS approach is the most practical: by factoring out the incidental details (the "syntactic sugar") as a translation ("desugaring") to a kernel language, any work you do on the formal semantics of the language only has to focus on the smaller kernel.
This is also a really practical way to approach building tools for JS, like static analysis: if you design a single desugaring pass as a translation, then you can build a whole bunch of tools on the kernel language. Same idea roughly as the standard compilers approach of translating to an IR.