Verified OCaml Library – VOCAL

Our project aims at developing the first mechanically verified library
of efficient general-purpose data structures and algorithms. This may
come as a surprise, but there does not currently exist any
verified library of significant size in any programming language.
In the recent decades, a lot of effort has been invested into the
development of program verification tools for mainstream languages
such as C or Java, including efforts by members of our teams.
These efforts have been successful in a number of specific application
domains, and they are relevant (and even necessary) for the purpose of
verifying low-level code. However, the task of
verifying, and even specifying, code written in such languages is often
severely burdened by the intrinsic complexity of the semantics of
the underlying programming model, such as the numerous possibilities
for memory access patterns in the C language. This complexity
probably explains in part the lack of verified libraries for such
languages.

Instead, we plan to target OCaml, a programming language whose programming
model makes it relatively easier to reason about programs, while preserving
the ability to produce fairly efficient code.
These features of OCaml explain that it has
been adopted world-wide for scientific, engineering, and financial
software systems where stability, safety and correctness is of utmost
importance. Examples include the Coq proof assistant, the Astrée and
Frama-C static program analyzers, the CompCert optimizing C compiler,
the Alt-Ergo theorem prover, financial software at Jane Street and
Lexifi, or the Coccinelle semantic patch engine. The clean and simple
semantics of the OCaml programming language reduces the effort
involved in program verification, and this has motivated us in the
recent years to focus on the development of verification tools
targeting this language. These tools have now reached a degree of
maturity that we believe makes them ready to tackle the challenge of
developing a realistic, fully verified library of data structures and
algorithms.

Although we target OCaml code, the result of our effort will not
benefit only the OCaml community. Indeed, specifications and proofs of
algorithms and data structures are, to a large extent, independent of
the programming language. For example, a priority queue
implemented in C would have essentially the same specification and
invariants as its OCaml counterpart. Although in this project we plan
to focus only on OCaml code, we believe that our work could be later
reused, to a large extent, for developing formally verified libraries
in other languages, or, even better, for developing cross-language
bases of formally verified code.

Our library, which will be entirely open source, will be readily
available for use by any OCaml programmer under a free software
license. In particular, it will be available to implementers of
safety-critical OCaml programs (e.g., Coq, Astrée, Frama-C, as well as
new projects). By offering verified program components, our work will
provide the essential building blocks that are needed to significantly
decrease the cost of developing new formally verified programs.

To carry out our project, we gathered a team of researchers and
programmers, all of whom have long experience in OCaml programming, Coq proofs,
and program verification. Compared with our prior experience in
program verification, we will particularly focus in this project on
modularity and reusability of specifications, and on the smooth
support of machine integers, which in many situations are critical for
obtaining efficient code that can be realistically integrated in
practical software.