In this work, we present a formal study on optimizing the energy consumption of energy harvesting embedded systems. To deal with the uncertainty inherent in solar energy harvesting systems, we propose the Stochastic Power Management (SPM) scheme, which builds statistical models of harvested energy based on historical data. The proposed stochastic scheme maximizes the lowest energy consumption across all time intervals while giving strict probabilistic guarantees on not encountering battery depletion. For situations where historical data is not available, we propose the use of (i) a Finite Horizon Control (FHC) scheme and (ii) a non-uniformly scaled energy estimator based on an astronomical model, which is used by FHC. Under certain realisti...