Adventures with formally verified Coq code and unverified OCaml code


David Monniaux, CNRS - Laboratoire Verimag. 12 mars 2025 10:00 TLR limd 2:00:00
Abstract:

It is commonplace to split a complex, formally verified piece of software (e.g., CompCert) into a formally verified part (e.g. written in Coq/Rocq) and an unverified part (e.g., written in OCaml). There are many pitfalls when doing this (types of values exchanged, assumptions of purity, modeling of pointer equality…). We shall in particular discuss situations where the unverified part submits a result, together with an optional certificate, to a verified checker, and illustrate them with examples from the Verified Polyhedra Library and CompCert- Chamois .