Frama-C est une plateforme open source et extensible d'analyse de code source C. Ses fonctions s'ajoutent par des greffons, dont Eva, WP et E-ACSL, qui assurent l'analyse de valeurs, la vérification déductive et le contrôle à l'exécution. Les équipes de développement et de vérification l'utilisent pour contrôler que le code C se comporte conformément à sa spécification. Le projet publie ses nouvelles versions sous forme de releases numérotées sur son site.
Frama-C est développé par le CEA-List, laboratoire du Commissariat à l'énergie atomique et aux énergies alternatives (CEA), avec l'Inria, institut public français de recherche en sciences du numérique. Aucun de ces organismes n'est une société détenue par un actionnaire étranger, de sorte qu'aucune société mère non européenne n'intervient. Le code est en grande partie sous licence LGPL et certaines parties sous licences BSD, ce qui permet aux organisations de l'examiner, de l'héberger et de l'adapter. Pour une organisation européenne, c'est un outil open source qui fonctionne sur ses propres systèmes. Le site du projet ne décrit aucun service hébergé.