Popular repositories

1. gospel gospel Public

   A tool-agnostic formal specification language for OCaml.

   OCaml 116 16

2. cameleer cameleer Public

   A Deductive Verification Tool for OCaml Programs

   OCaml 56 8

3. ortac ortac Public

   Runtime assertion checking based on Gospel specifications

   OCaml 34 10

4. vocal vocal Public

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

   OCaml 15 3

5. why3gospel why3gospel Public

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

   OCaml 9 2

6. gospel2cfml gospel2cfml Public

   OCaml 1