Numerous roadblocks can be encountered when managing projects directed at deploying complex computer-based systems, or systems of systems (SoS), bound to operate autonomously. Existing system engineering (SE) methods and supporting tools are not applicable as they stand for mastering the complexity involved with modern (current, future) applications and/or operations, in the civilian domain as well as in the defense domain. We report on the outcomes of a study sponsored by French DGA, directed at investigating issues raised with autonomous systems, such as robots or drones, as well as with systems of such systems, such as fleets or swarms of terrestrial, or underwater, or aerial, autonomous systems. This study should be continued and expanded under a European programme. Slashing the acquisition costs of autonomous systems has been the primary motivation for the launching of this study, hence the focus on openness and interoperability. It was also decided to test the applicability of formal/scientific proof-based SE (PBSE) methods for managing the lifecycle of such systems. One goal pursued during this study was to explore the following double conjecture: (1) Is it the case that greater reliance on, and exploitation of, exact sciences should help circumvent the weaknesses intrinsic to current SE methods? (2) If the case, how to "hide" the introduction of exact sciences within the SE processes followed by engineers working on a project? The fact that autonomy and interoperability were two major keywords in that study matched ideally with the goal of exploring PBSE methods, since proofs of stipulated properties (future operational behaviours) are of utmost importance with systems and SoS meant to operate autonomously, in cooperation with others, be they the result of SE work planned ahead of time, or be they ad hoc SoS, set up in limited time in operational theatres. The role of manufacturers of robots and drones which participated into the study was triple. Firstly, they were responsible for bringing in real world scenarios of SoS in three domains (aerial, terrestrial, underwater). Secondly, they had to participate in the deployment of the PBSE methods for these SoS. Thirdly, they had to draw conclusions from their direct exposure to PBSE. French DGA was also directly involved, in order to gain a better understanding of what PBSE may offer to a prescribing authority. The study has produced convincing cases in favour of PBSE, from both a "theoretical" viewpoint and a "practical" viewpoint. On the "theoretical" side, it was demonstrated that semi-formal PBSE methods are inevitable, given that current formal PBSE methods suffer from limitations, especially regarding (1) requirements capture phases, (2) identification of generic problems and solutions, (3) automated reuse of existing design solutions and proofs during system design & validation phases. A rather encouraging lesson has been learned: When combined together, formal and semi-formal PBSE methods can encompass an entire project lifecycle, maintaining a continuous "proof chain" all the way through. On the "practical" side, besides meeting the contractual goals, such as showing how to encapsulate scientific results in order to make them "one click away" for project engineers, the study led to the inception of a novel lifecycle model, rooted into PBSE principles, while being fully compatible with popular SE lifecycle models, such as, e.g., ISO/IEC 15288. Hence, regarding standards, the study reached beyond the intended goals. Rather than delivering proposals for technical standards only, the PBSE-centric lifecycle model turned out to be a quite attractive basis for a methodological standard. This resulted into the OISAU methodological standard for open interoperable autonomous systems and SoS.