Frama-C is een open-source, uitbreidbaar platform voor de analyse van C-broncode. Functies worden toegevoegd via plug-ins, waaronder Eva, WP en E-ACSL, die waardenanalyse, deductieve verificatie en controles tijdens de uitvoering ondersteunen. Ontwikkel- en verificatieteams gebruiken het om te controleren of C-code zich gedraagt zoals de specificatie beschrijft. Het project publiceert nieuwe versies als genummerde releases op de website.
Frama-C wordt ontwikkeld door CEA-List, een laboratorium van de Franse Commissariat à l'énergie atomique et aux énergies alternatives (CEA), samen met Inria, een Franse publieke onderzoeksinstelling voor digitale wetenschap. Geen van beide is een bedrijf met buitenlandse eigenaar, dus er is geen niet-Europese moedermaatschappij betrokken. De code valt grotendeels onder de LGPL en deels onder BSD-licenties, zodat organisaties de code kunnen inzien, zelf hosten en aanpassen. Voor een Europese organisatie is het een open-source hulpmiddel dat op de eigen systemen draait. De projectsite beschrijft geen gehoste dienst.