github.com/lthms/FreeSpec ↗
A framework for implementing and certifying impure computations in Coq
Open this visualization on its own page →
Contributors
5
Lines of Code
1,907
From
2017-05-31
To
2020-12-16
About lthms/FreeSpec
FreeSpec is a Coq framework for implementing and formally verifying impure computations, addressing the challenge of reasoning about side effects in a pure theorem prover. The project provides three main packages: coq-freespec-core supplies the foundational formalism for modeling impure operations, coq-freespec-exec enables the execution of such certified computations, and coq-freespec-ffi integrates with coqffi for foreign function interfaces. The codebase includes Coq theory definitions, OCaml plugins, and practical examples demonstrating each component.
The framework is built on the concept of freer monads, allowing developers to specify effects abstractly and prove properties about programs that use them. It depends on coq-ext-lib for core extensions and optionally on coqffi for FFI support. The project includes testing infrastructure and generates both OCaml and Coq documentation that is published online.
FreeSpec was developed at France's ANSSI cybersecurity agency and is distributed under the MPL2 license. The work is grounded in peer-reviewed research, with two published papers describing the formalism and its applications to modular verification of programs with effects and effect handlers.