Formal verification of embedded system software can profoundly influence both safety and security, and has the potential to alter the development process substantially. However, the complexity of formal verification, along with stringent time-to-market and resource constraints of embedded systems, has posed significant barriers to its adoption. Moreover, ensuring the accessibility of formal methods in the design and implementation of embedded systems remains a major challenge. In our paper, we evaluate formal methods and demonstrate the accessibility and benefits within a critical area of many industries: IEEE754 floating-point values are widely used and due to their fixed size, they can only approximate real numbers. For the most part, their behavior aligns with programmer expectations; however, certain corner cases exist in which they are susceptible to value cancellation, rounding errors, and deviations from standard mathematical rules. Such discrepancies can be problematic when calculated results diverge from software developer expectations, potentially leading to fatal errors. We propose SafeFloatZone which allows for the identification of safe domains for algorithms utilizing IEEE754 floating-point numbers. The approach is rooted in formal verification, leveraging modern, efficient Satisfiability Modulo Theories (SMT) solvers to deduce preconditions for functions, thereby providing stronger guarantees of correctness. In this work we demonstrate how SafeFloatZone can readily benefit embedded system developers and show that it is transferable to a variety of algorithms based on IEEE754 floating-point numbers.