package gospel

  1. Overview
  2. Docs
A tool-agnostic formal specification language for OCaml


Dune Dependency







  • Created a gallery of Gospel examples that might serve as a working ground to experiment with Gospel syntax and future extensions of the language. [#361] (


  • Make the type-checker save type information in a file #376

  • Make the with necessary when declaring type invariants #372 and #374


  • Fix premature parsing of specification keywords in the preprocessor. #394

  • Fix ls_name of unit logical symbol to be () #387

  • Fix the is_ts_tuple function so that it doesn't take unit to be a tuple #386

  • Use unique identifiers rather than physical equality for Symbols.ls_equal #380

  • Remove the gospel_expected prologue at the end of successful tests #363



  • Introduce a generic pp_gen pretty-printer for error messages, so that external tools can pretty-print errors in the same style #326

  • Add ppx rewriter to display gospel contents as documentation with odoc #288

  • Add specific error message for patterns with guard on every clause. #220

  • Added when guards in pattern-matching #206

  • Added a with construct to name a variable in type invariants referring to a value of the specified type. #218 and #187

  • Added support for int literals. #175 and #177 and #223

  • Added the Failure exception to the Stdlib. #154

  • Added a gospel dumpast command. #98 and #184


  • Forbid old operator in precondition clauses (requires and checks) #335

  • Display a warning when encountering an include #334

  • Allow patterns in arguments and return type annotation in anonymous functions #309

  • Propagate pattern locations to report errors to the precise patterns #308

  • Support partial application of functions and enforce OCaml syntax for constructor application #290

  • Add a pretty-printer for locations #294

  • Gospel preprocessor does not fail when the file is an implementation file #265

  • Rename standard library Seq and 'a seq to Sequence and 'a sequence. #253

  • Allow unit result in function header #215

  • Highlight source locations when reporting errors. #214

  • Check for pattern-matching redundancy in terms. #213

  • Check for pattern-matching exhaustivity in terms. #170

  • Issue a warning when a function returns unit but has no modifies clause. #185

  • Improved locations for syntax errors in specs. #164

  • Documentation improvements. #108 and #110 and #149

  • Added sanity checks to type invariants: invariants are only allowed on private or abstract types. #117 and #116

  • Stdlib changes. #102

    • Removed ref operator.

    • Removed elements for Bag and Set.

    • compare functions returns integers instead of ints.


  • Fix the performance issues in the preprocessor \353

  • Gospel preprocessor support documentation for ghost declaration #331

  • Consider comments as spaces while preprocessing (to ensure specification can be attached to a ghost function or type, for instance) #321

  • Fix source-location tracking (directives and overridden filename) #319

  • Set up location in parsing ghost specifications #310

  • Check that all patterns in a disjunction bind the same variables #300

  • Handle the special case of MODULE_ALIASES in stdlib.mli in the parser #306

  • Take recursivity into account when typing type declarations #304

  • Support pattern with cast #301

  • Use payload location for specification text #299

  • Support patterns of one-parameter constructors with a tuple argument #297

  • Use correct location for arity mismatches in type applications #258

  • Avoid uncaught exception when displaying a warning for builtins (using Location.none) #283

  • Gospel preprocessor no longer detach documentation below a declaration #281

  • Fixed pattern match analysis in exceptional postconditions #277

  • Avoid uncaught exception when displaying a warning on a dummy position #262

  • Constants can now be referenced in specifications. #211

  • Infix operators in specificaion headers are now accepted. #205

  • Fix inconsistencies in typing/parsing of exceptional postconditions patterns. #203

  • Fixed the type-checking of interfaces involving the OCaml Stdlib, which was not opened by default. GADTs are considered abstract types. #195

  • Fixed incorrectly rejected interfaces with absent\partial function contracts in the presence of tuples as return values. #193

  • Fixed support for types containing functions. #186

  • Fixed wrong syntax errors in patterns. #181

  • Fixed wrong invalid patterns over unit values. #174

  • Fixed the error message for pattern type errors. #172


  • Display the backtrace of an error when $GOSPELDEBUG is set #295

  • Fixed the order of exceptional postconditions in the AST. #200

  • Refactored the error handling: Gospel now only raises a single Gospel.Error exception. #189

  • Fixed the representation for type variables in ts_tuple and fs_tuple. #183

  • Added int as a primitive type. #171

  • Refactored Tterm and Symbols. #85

  • Redefined the ghost type. #155

  • Removed the Pty_open type constructor #109

0.1.0 (11-03-2021)

  • Initial release


Innovation. Community. Security.