Syntéza programů je automatické sestavování programu podle zadání, příkladů vstupů a výstupů nebo pravidel, která má výsledek splňovat. Systém hledá kombinaci povolených operací a ověřuje ji vůči těmto podmínkám. Nemusí přitom vznikat běžný zdrojový kód: program může popisovat i postup složení objektu nebo sled jeho úprav. Syntéza může používat prohledávání, logické řešiče i modely strojového učení; není tedy totéž co obecné programování pomocí chatbota. Zatímco formální verifikace prověřuje správnost již daného programu, syntéza se snaží vhodný program nejprve vytvořit. Spolehlivost výsledku závisí na přesnosti zadání a důkladnosti kontroly.
