FreeSpec

FreeSpec is a compositional reasoning framework for the Coq proof assistant. It aims at providing facilities to modularly implement, specify and verify complex systems built with a collection of interconnected components.

Although FreeSpec remains a work-in-progress, efforts have been made to ensure interested users can already use it.

Documentation

• In accordance with Coq community best practice, the codebase has been heavily commented, and pretty-printed thanks to coqdoc. [Read more]
• FreeSpec provides a plugin called FreeSpec.Exec, whose main feature is to be extensible. [Read more]