The standardized operations, e.g. multiplication or square root extraction, are precisely defined, i.e. the result is always defined exactly, by the combination of the corresponding operation with real numbers and by the rounding rule that is applied.

IEEE 754 also contains a list of operations that are recommended, but not defined by the standard, such as the exponential function and other functions where it is difficult to round exactly the result.

For the standardized operations, all the possible errors are precisely defined and they must either generate an appropriate exception or produce as result a special value that encodes the kind of error, depending on how the programmer configures the processor.

The standard is perfectly fine. The support of the standard in the popular programming languages is frequently inconvenient or only partial or even absent. For instance it may be impossible to choose to handle the errors by separate exception handlers and it may be impossible to unmask some of the exceptions that are masked by default. Or you may lack the means to control the rounding mode or to choose when to use FMA operations and when to use separate multiplications.

If you enable all the possible exceptions, including that for inexact results, the value of an expression computed with IEEE 754 operations is the same as if it were computed with real numbers, so you do not need to prove anything extra about it.

However this is seldom helpful, because most operations with FP numbers produce inexact results. If you mask only the exception for inexact results, the active rounding rule will be applied after any operation that produces an inexact result.

Then the expression where you replace the real numbers with FP numbers is equivalent with a more complex expression with real numbers that contains rounding operations besides the explicit operations.

Then you have to prove whatever properties are of interest for you when using the more complex expression, which includes rounding operations.

The main advantage of the IEEE 754 standard in comparison with the pathetic way of implementing FP operations before this standard, is that the rounding operations are defined exactly, so you can use them in a formal proof.

Before this standard, most computer makers rounded the results in whatever way happened to be cheaper to implement and there were no guarantees about which will be the result of an operation after rounding, so it was impossible to prove anything about FP expressions computed in such computers.

If you want to prove something about the computation of an expression when more exceptions are masked, not only the inexact result exception, that becomes more complex. When a CPU allows a non-standard handling of the masked exceptions, like flush-to-zero on underflow, that can break any proof.