Human spaceflight operations challenge currently available planning technology. They typically rely on a large number of integrated functions including mission planning, crew planning, solar array management, power and thermal management and system health monitoring. These functions serve under heterogenous uncertainties (stemming from anomalies and faults in equipment and intrinsic unknowns about the environment), time-varying requirements and multiple, possibly competing objectives. Co-work with the crew introduces unique difficulties as well. Humans’ capabilities and limitations in these capabilities add to the uncertainties. Humans’ preferences and need for compatibility between the humans and autonomous control protocols introduce unconventional constraints. The proposed effort introduces a paradigm shift in the planning-execution loop by addressing a number of these challenges. Our emphasis particularly on unambiguous, formal specifications and compilation of executable control software with provable guarantees and systematic sensitivity analysis diffuses the critical concern of reliability throughout the planning execution loop. The proposed algorithms will incorporate models with stochastic as well as nondeterministic uncertainties and rich specifications with temporal and logical relations as well as probabilistic and real-time modalities as needed. Integrated planning for the coupled functions introduces possibilities for system-level optimization, e.g., in performance, weights and overall cost. Finally, the proposed algorithmic and architectural advances will improve not only the scalability of the resulting synthesis algorithms but also their interpretability by and explainability to the crew and designers.