Popular repositories Loading

1. gospel gospel Public

   A tool-agnostic formal specification language for OCaml.

   OCaml 133 16

2. cameleer cameleer Public

   A Deductive Verification Tool for OCaml Programs

   OCaml 67 8

3. ortac ortac Public

   Runtime assertion checking based on Gospel specifications

   OCaml 44 10

4. vocal vocal Public

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

   OCaml 16 2

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. peter peter Public

   Translation tool that converts Gospel Specifications into CFML.

   OCaml 3