github.com/uwplse/cheerios ↗
Formally verified Coq serialization library with support for extraction to OCaml
Open this visualization on its own page →
Contributors
8
Lines of Code
705
From
2016-02-05
To
2020-01-31
About uwplse/cheerios
Cheerios is a formally verified serialization library for Coq that enables developers to define and prove properties of serializable types. It provides a typeclass-based framework with built-in instances for many standard library types, allowing users to serialize and deserialize data while maintaining formal guarantees about correctness. The library is compatible with Coq 8.14 and later, and depends on StructTact as an additional requirement.
The library supports extraction to OCaml, making it possible to use formally verified serialization in executable programs. To do this, developers extract their Coq code to OCaml and link it with the Cheerios runtime library, with the connection between Coq definitions and runtime primitives established through the `ExtractOCamlCheeriosBasic.v` module. The project includes both the main Coq library and a separate OCaml runtime component that can be built with OCamlbuild.
Cheerios targets users working in formal verification who need serialization capabilities with proof support, as well as developers building systems that require both executable code and formal correctness guarantees. The project is maintained under a BSD 2-Clause license and can be installed via opam or manually compiled.