Welcome to the FoCaLiZe website. This site offers information about FoCaLiZe, some documentation about the language and its compiler, some training opportunities, and of course, the latest release of FoCaLiZe.

Mirrors: INRIA, ENSTA, ENSIIE ( currently down).


The FoCaLiZe project aims at providing a programming environment to develop certified programs. The environment is based on a functional programming language with object-oriented features. The language allows the programmer to write formal specifications and proofs of the program in a unified and consistent setting.

From a FoCaLiZe source code development, the focalizec compiler produces three source files:

Thanks to built-in inheritance mechanisms, the language allows to refine a development from the coarse-grain specification to the fully defined executable program.

The FoCaLiZe distribution includes a library of mathematical algebraic structures up to multivariate polynomial rings, a library of security policies and various examples contributed by FoCaLiZe users. The resulting libraries are noticeably efficient; for instance, the complex algorithms of the algebraic library provide runtime performances comparable to the best Computer Algebra Systems available.

New release (0.9.0) of the FoCaLiZe environment (2014-10-14)

The new release of the FoCaLiZe environment, focalize 0.9.0, is now available. A certain number of bugs found in the focalizec compiler have been fixed and Zenon also had several issues fixed. Final let-definitions are now integrated. The computation of dependencies has been deeply rewritten to compute them *once* for all the possible backends (OCaml, Coq). Generated code is slightly lighter and naming schemes and code generation schemes have been standardized between OCaml and Coq. A complete description of changes / new features can in found in the CHANGES file of the distribution.

Server issue and migration (Sept-Oct 2014)

Due to an issue on the old server hosting FoCaLiZe, the site was down during some weeks. The situation is now back to a normal state after a migration. Only the bugtracker is still down and will be fixed soon.

Slides and Lecture Notes of EJCP 2014 (2014-09-08)

The material of the course given at Ecole des Jeunes Chercheurs en Programmation (EJCP) in May 2014 is now available via the Documentation page. This document introduces the aims of proving software and shows application using FoCaLiZe.

Update of tutorial "Playing with proofs" (2014-03-06)

The tutorial "Playing with Proofs" available in the distribution and via the Documentation page has been updated to make the proof dealing with tree mirror working again. We still have to add few words to explain clearly how to state induction hypotheses in case of multiple recursive calls. Some words also have to be added about the shape of the goals and the equivalent shapes they can have to allow Zenon to use induction. Will be done ASAP ;)

Fixed broken links to papers in resources (2014-02-14)

Due to a site migration, some links to papers available in the Resources page got broken. The PDF files are now back.

final let-definitions available (2014-01-31)

A new feature is now available (currently only from the GIT repository) allowing to forbid redefinitions of let-definitions (logical or not): the final qualifier. This feature was requested to avoid duplicating the code of a logical let by adding a theorem paraphrasing the definition's body in order to prevent further redefinitions from changing the definition. For sake of homogeneity, "final-ity" is available also for "non-logical" definitions.

The following code*:
  logical let is_A_singleton = all a : A, A!equal (a, A!element);
  (* Theorem to avoid changes of is_A_singleton. *)
  theorem is_A_singleton_spec :
     is_A_singleton <-> all a : A, A!equal (a, A!element)
  proof = by definition of is_A_singleton ;

may now be simplified in:

  logical final let is_A_singleton = all a : A, A!equal (a, A!element);

Since no children in the inheritance will be allowed to alter the "meaning" of is_A_singleton, the theorem is_A_singleton_spec is no more needed.

(*) Thank's to Mathieu and Théo for the example.

Fix of the Zenon GIT repository (2014-01-17)

Zenon GIT repository got corrupted causing an incorrect git clone when used as anynymous user via the http link provided in the Download page. The version that was fetched did not include number of (more or less) recent commits, hence did not make available bug fixes and features of Zenon.

This is now fixed, users can clone or update their version of Zenon. Versions prior to 0.7.2 [a257] 2014-01-05 are out-of-date and were possibly impacted by the repository corruption.

Split of FoCaLiZe and Zenon GIT repositories (2013-04-08)

FoCaLiZe and Zenon are now in two separate GIT repositories. This won't impact the available material but now requires to clone both repositories. This split allows lighter installation when only needing Zenon. Until Zenon's repository is cleanly integrated as a sub-module of the FoCaLiZe one, these two separate clone/pull/push processes are required.

Bug tracking now available (2013-01-21)

Bugs, feature requests etc. can now be submitted via the FoCaLiZe bug tracker (powered by Bugzilla). We encourage this process instead of direct mails since it allows keeping trace of requests, prevents "memory loss" (the post-it stuck on the screen and finally falling down in the bin or whatever else) and can be used as knowledge database before submitting new requests.

Extended tutorial "Playing with Proofs" (2013-01-21)

The online version of the tutorial about proofs now contains a section dedicated to explicit induction, i.e. when Zenon does not succeed in finding a proof in a fully automatic way. This section shows how to apply the usual scheme of proof by induction, proving base cases, then induction cases under induction hypotheses.

New release (0.8.0) of the FoCaLiZe environment (2013-01-10)

The new release of the FoCaLiZe environment, focalize 0.8.0, is now available. FoCaLiZe got nearly asleep for some years, without major release despite some underground works. The "ghost" 0.7.0 version never became public, but the 0.8.0 cumulating the evolutions of the repository is nearly ready. Get the last version from the Download page and the related documentation from the Documentation page.
After a pretty long time without release, this new version brings number of enhancements, from the focalizec compiler and Zenon. New versions of OCaml and Coq are now supported as well as previous ones for sake of legacy. Zenon made impressive progress so as to be helpful in proving inductive properties for species. Installation and setup have been fully revisited, leading in a simpler and lighter mechanism. The standard library has been extended with low-level theorems. Termination proofs for structurally recursive functions are now possible. A certains number of bugs found in the focalizec compiler have been fixed. And a new tutorial about making proofs with Zenon is born. A complete description of changes / new features can in found in the CHANGES file of the distribution.

Initial event: The SSURF ANR project

The SSURF (Safety and Security UndeR Focal) ANR project was the starting point of the concretization of the FoCaLiZe environment, leading to an effective implementation of what is now the focalizec compiler, greatly helped by Zenon.
As a summary, this project consisted in :

Further information (in french) can be found here.

Last modification date: Tuesday, October 14th, 2014 on host dhcpuei9.ensta.fr by user didou.
Copyright © 2005 - 2014 INRIA & LIP6, 2012 - 2014 ENSTA ParisTech, all rights reserved.