Ist es denn garantiert durch alle bisherigen Sprachversionen von JS so, dass die "Addition" von "1" und "2" keinesfalls "3", sondern immer "12" ist?

Ja, sobald ein Operand ein String ist, ist das garantiert.

Hier sind sogar beide Operanden Strings – denn die value-Eigenschaft gibt immer nur Strings zurück.

Ja, das ist seit ECMAScript Edition 1 (1997) so standardisiert:
http://www.ecma-international.org/publications/files/ECMA-ST-ARCH/ECMA-262, 1st edition, June 1997.pdf
Siehe 11.6.1 The addition operator ( + ), Seite 43, Schritt 7:
»7. If Type(Result(5)) is String or Type(Result(6)) is String, go to step 12.
[…]
12. Call ToString(Result(5)).
13. Call ToString(Result(6)).
14. Concatenate Result(12) followed by Result(13).«

Vergleich ECMAScript 5.1, 14 Jahre später:
http://www.ecma-international.org/ecma-262/5.1/#sec-11.6.1
»7. If Type(lprim) is String or Type(rprim) is String, then
  a. Return the String that is the result of concatenating ToString(lprim) followed by ToString(rprim)«

Grüße
Mathias