Popular repositories Loading

1. gospel gospel Public

   A tool-agnostic formal specification language for OCaml.

   OCaml 162 19

2. cameleer cameleer Public

   A Deductive Verification Tool for OCaml Programs

   OCaml 85 11

3. ortac ortac Public

   Runtime assertion checking based on Gospel specifications

   OCaml 55 10

4. vocal vocal Public

   Vocal is a set of OCaml modules, formally verified using Gospel and its Why3 plugin.

   OCaml 19 3

5. why3gospel why3gospel Public

   A Why3 plugin able to read and translate Gospel specifications, in view of refinement proofs of Why3 programs.

   OCaml 11 2

6. peter peter Public

   Translation tool that converts Gospel Specifications into CFML.

   OCaml 4