Frama-C ist eine quelloffene, erweiterbare Plattform zur Analyse von C-Quellcode. Funktionen werden über Plug-ins ergänzt, darunter Eva, WP und E-ACSL für Wertanalyse, deduktive Verifikation und Laufzeitprüfung. Entwicklungs- und Verifikationsteams nutzen sie, um zu prüfen, ob C-Code sich wie in seiner Spezifikation beschrieben verhält. Das Projekt veröffentlicht neue Versionen als nummerierte Releases auf seiner Website.
Frama-C wird vom CEA-List entwickelt, einem Labor des französischen Kommissariats für Atomenergie und alternative Energien (CEA), gemeinsam mit Inria, einem französischen öffentlichen Forschungsinstitut für Digitalwissenschaften. Keiner der beiden ist ein Unternehmen mit ausländischem Eigentümer, daher ist keine außereuropäische Muttergesellschaft beteiligt. Der Code steht überwiegend unter der LGPL und teilweise unter BSD-Lizenzen, sodass Organisationen ihn prüfen, selbst betreiben und anpassen können. Für eine europäische Organisation ist es ein Open-Source-Werkzeug, das auf eigenen Systemen läuft. Die Projektwebsite beschreibt keinen gehosteten Dienst.