Although large language models (LLMs) are becoming increasingly capable at coding, ensuring the formal correctness of their output remains a major challenge. We present Autofy, a system that orchestrates multiple LLM roles to synthesize SPARK/Ada programs that (i) compile, (ii) pass formal verification and (iii) satisfy functional tests. Autofy integrates Alire for project bootstrap, GNAT/GCC and gnatpp for style/syntax/semantics checks and compilation, GNATprove for formal verification, as well as functional tests to ensure guard-railed results. Two complementary flows are supported: a \emph{Multi-Version} approach that cross-combines independent contract and implementation variants, and a \emph{Director-Feedback} approach in which a Director LLM reads compiler/prover/test logs and emits targeted edits. In evaluations across multiple datasets and models, Autofy solved up to 31% (\emph{Multi-Version}) / 71% (\emph{Director-Feedback}) of SPARK coding tasks - substantially outperforming naive prompting (5%). We discuss system design, empirical results, and open challenges for combining LLMs with sound software engineering and formal methods.