We had yesterday our first joint meeting in Hi-Lite since the start of the project, 6 months ago. This was the occasion for CEA to present their ideas for E-ACSL (the executable fragment of the ACSL specification language for C) and for us at AdaCore to present our ideas for ALFA (the subset of Ada 2012 that will be suitable for formal verification).
The overall directions have been agreed by all partners. In particular, we agreed on the vision of a product that allows unit testing and/or unit proof on individual functions from a program, depending on the features of C/Ada exercized in the function. This will be a major departure from other formal verification tools and methodologies (SPARK, B method) allowing a finer-grain choice of what should be formally verified and what should be tested.
Discussions on E-ACSL and ALFA are expected to continue on the public mailing list hi-lite-discuss@lists.forge.open-do.org.