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.