Monads in Haskell serve two purposes.
A monad that is defined within Haskell is really a simulation of some computational effect in terms of pure (side-effect free) computation. After all, Haskell is a pure language.
The second use of monads in Haskell, as well as in programming language semantics, and many other languages, is to model external or primitive computational effects. Such effects cannot be defined within the language itself. They necessarily come from some external environment (hardware, operating system, virtual machine).
In Haskell the monad that gives access to external effects is IO. This is why the main program has the type IO () – so that it can actually interact with the external world through computational effects.
Under the hood, the Haskell compiler compiles pure code, including user-defined monads, to machine code that behaves equivalently to the pure code (with respect to a formal semantics). But it takes special care of code of type IO by compiling things like putStr to actual system calls that trigger real I/O (I am over-simplifying a bit, but you get the point).
The ML-family of languages differ from Haskell because they do not separate so cleanly the pure & effectful computations. In such "impure" languages, all computations happen in a single IO-style monad that gives access to all external effects (I/O, mutable memory, exceptions) all the time. And the fact that this is the case is not recorded in types. Thus, an ML computation of type int would really be something like IO Int in Haskell.
Of course, the programmer is free to define their own monads in ML to simulate various computational effects, just like in Haskell, but this is a bit irrelevant here.
You ask how the effects are specified in the formal semantics. There are several ways of doing it (transition semantics, algebraic semantics, abstract interpretation), and I am not sure that describing them here would serve a purpose. Please ask for further references if you'd like to know the details.
The important thing to understand is the relationship between the formal semantics, which is the mathematical model of computational effects, and the actual implementation by the language compiler, which converts source code to machine code that triggers computational effects by using the available hardware, possibly via some system calls. We want the mathematical model and the compiled code to match, i.e., the compiler should be correct with respect to the formal semantics.