The BLESS Manual contains:

  • a language reference manual with formal grammar and semantics,
  • a guide to the BLESS tool,
  • and soundness proof for a growing list of proof rules.

Sometimes, a quick look at BNF grammar helps figure out how to express what you want. Six syntax cards are provided: the combined BLESS grammar, and the grammars for each of the annex languages: Action, Axiom, State Machine, Type, and Unit.