Project Hi-Lite


Project Hi-Lite has ended!

To download the SPARK Hi-Lite GPL 2013 release, go to

To download the Fluorine Frama-C release, with the associated E-ACSL plug-in, go to

To follow developments of SPARK 2014, go to

To follow developments of Frama-C, go to

Final project reports

Slides presented during the final project meeting on May 29th, 2013


Hi-Lite is a project aiming at popularizing formal methods for the development of high-integrity software. It targets ease of adoption through a loose integration of formal proofs with testing and static analysis, that allows combining techniques around a common expression of specifications. Its technical focus is on modularity, that allows a divide-and-conquer approach to large software systems, as well as an early adoption by all programmers in the software life cycle.

Hi-Lite is completely based on libre software. The project is structured in two different toolchains for Ada and C based on GNAT/GCC compilers, the SPARK verification toolset and the Frama-C platform. The integration of these toolchains inside two industrial IDEs offers to the user a common interaction on Ada and C programs. In particular, mixed Ada/C programs can be verified against a common specification.

Project Hi-Lite has officially launched and we will be reporting on its progress here as it reaches major milestones throughout the evolution of the project.

To get started on Hi-Lite, see

A "Lighter" Introduction to Hi-Lite

Hi-Lite is based on powerful industrial tools that have been developed by the different partners for the last 10 to 25 years. In order to show you how Hi-Lite can improve on the existing state-of-the-art by creating new communications between these tools, we describe in the following the application of the various tools and techniques that are part of Hi-Lite to a very simple program.

For the full story: Click here »

Related Initiatives

The OpenETCS project aims at integrating modeling, development, validation and testing in a common framework around open-source tools. See the GNATprove description at ETCS github repository.

The Workshop on Theorem Proving in Certification is now organized as a recurring event to compare approaches and tools based on theorem proving to critical software (such as avionics software), where a certification standard applies (DO-178B/C for avionics software). Here is the 2010 workshop and the 2011 workshop.

The tool ImProve performs formal verification (via model checking) on a small Embedded Domain Specific Language inside Haskell, and code generation to C.


Hi-Lite is an Open Source project financially supported by the French Government and the Essone general council in an effort to increase the use of formal methods in developing high-integrity software, particularly to meet the forthcoming DO-178C avionics standard.


The project partners are AdaCore, Altran, Astrium Space Transportation, CEA-LIST, the ProVal team of INRIA and Thales Communications. AdaCore is the project leader.

For more information on partners: Hi-Lite Partners Page »


Hi-Lite: a Verification Toolkit for Unit Test & Unit Proof
A presentation by Yannick Moy, Senior Engineer, AdaCore, at a talk at IRILL Days 2010. Video courtesy of IRILL (

An Introduction to Open DO
A presentation by Cyrille Comar, Managing director of AdaCore Europe

You can also view the presentation slides if you want to follow along. Note that the Hi-Lite slides start on page 30..

More Resources

For the latest news and events on Project Hi-Lite: Hi-Lite News and Events Page »

For the latest papers and presentations on Project Hi-Lite: Hi-Lite Resources Page »

To watch recent progress made in Project Hi-Lite: Hi-Lite Progress Page »

Get Involved

To get (read) access to the git repository, look at Open-DO Forge »

To participate in the technical discussions, subscribe to Hi-Lite mailing-list »


For more information about project Hi-Lite:

  • Categories

  • Open-DO Projects

  • Contact

    info @