Skip to content

@ocaml-gospel ocaml-gospel

Change the repository type filter

All

    Repositories list

    8 repositories

    • ortac

      Public
      Runtime assertion checking based on Gospel specifications
      ocamlspecificationruntime-verificationverfication
      OCaml
      •
      MIT License
      •10•38•20•5•Updated Nov 13, 2024Nov 13, 2024

    • gospel

      Public
      A tool-agnostic formal specification language for OCaml.
      OCaml
      •
      MIT License
      •16•128•36•18•Updated Oct 7, 2024Oct 7, 2024

    • peter

      Public
      Translation tool that converts Gospel Specifications into CFML.
      OCaml
      •
      MIT License
      •0•1•0•0•Updated Sep 29, 2024Sep 29, 2024

    • gospel2viper

      Public
      OCaml
      •0•0•0•0•Updated Sep 11, 2024Sep 11, 2024

    • cameleer

      Public
      A Deductive Verification Tool for OCaml Programs
      OCaml
      •
      MIT License
      •8•60•6•1•Updated Jun 25, 2024Jun 25, 2024

    • gospel-rfc

      Public
      OCaml
      •0•0•1•0•Updated Mar 14, 2024Mar 14, 2024

    • why3gospel

      Public
      A Why3 plugin able to read and translate Gospel specifications, in view of refinement proofs of Why3 programs.
      OCaml
      •
      MIT License
      •2•9•1•1•Updated May 6, 2022May 6, 2022

    • vocal

      Public
      Vocal is a set of OCaml modules, formally verified using Gospel and its Why3 plugin.
      OCaml
      •
      MIT License
      •2•16•1•0•Updated Nov 3, 2021Nov 3, 2021