Pantagruel

module HAIKU.

Poem = [Line].
Line = String.

scans? p: Poem ⇒ Bool.

A haiku is a poem of exactly three lines.

scans? p → #p = 3.

Each line has a prescribed number of morae; the numbers of morae go 5, 7, 5.

scans? p → morae (p 1) = 5
∧ morae (p 2) = 7
∧ morae (p 3) = 5.

where

A mora is like a syllable, but shorter; it is known in Japanese as 音. To evaluate a line we count its morae.

morae l: Line ⇒ Nat.

Pantagruel is a computer program designed to help human beings think and communicate rigorously.

The human thinker can write a description of some system of rules, propositions, or behaviours in Pantagruel’s syntax and the Pantagruel document checker will attempt to validate the description.

Pantagruel constrains the human thinker into some of the syntactic forms of first-order logic and computer programming. In doing so it is hoped that the thinker will encounter elements of their thought which require further precision.

Through some simple constraints on the introduction and use of terms, Pantagruel might be able to assist the thinker in eliminating certain kinds of ambiguity to which natural language is prone.

module CHECKOUT.

User.
Document.
owner d: Document ⇒ User.

A specification for a small document management system.

↝ Check out | u: User, d: Document.

A user may check out a document if they have permission to access it and it’s not currently checked out.

owner d = nobody ∧ has-perm? u d → owner′ d = u.
owner d ≠ nobody ∨ ¬(has-perm? u d) → owner′ d = owner d.

where

nobody ⇒ User.
has-perm? u: User, d: Document ⇒ Bool.

Where It Helps

Natural language sounds precise until you try to formalize it. Writing a specification forces you to confront the ambiguities hiding in plain English.

Software Features

“Accounts cannot have a coupon applied more than once.”

Any coupon at all—or any given coupon? Formalizing forces you to choose:

// Any given coupon can't be reused:
all a: Account, c: Coupon |
    ~(applied a c) -> ...

// Only one coupon, ever:
all a: Account |
    #(each c in coupons, applied a c | c) <= 1.

Business Rules

“A manager approves expenses over $500.”

You naturally write managers—but which one? The checker won’t let you gloss over the plural:

managers => [Manager].
approves m: Manager, e: Expense => Bool.
...
all e: Expense, amount e > 500 |
    approves managers e.

error: Type mismatch:
  expected Manager, got [Manager]

You need to choose: some m in managers, or one designated-approver?

Win Conditions

“The player with the most points wins.”

What about ties? You guard the invariant so it only applies once the game ends—but the checker still finds the real problem:

score p: Player => Nat0.
finished => Bool.
...
// The player with the most points wins.
finished ->
    all q: Player, q != winner |
        score winner > score q.

initially ~finished.
initially all p: Player | score p = 0.

$ pant --check game.pant
OK: Invariant '...' holds in initial state
FAIL: Invariant 'finished -> ...' violated
  by action 'End-Game' (reachable)
  Reachable trace:
    score Player_0 = 0
    score Player_1 = 0
    score Player_2 = 0

Game Actions

“A player draws a card at the start of their turn.”

From where? What happens to the source? Formalization forces you to name it:

~> Draw | p: Player.
---
some c in deck |
    hand' p = hand p + c
    and deck' = deck - c.

How It Compares

Pantagruel occupies a different point in the design space from established formal methods tools. Like them, it offers bounded model checking (via SMT solvers), but it prioritizes readability and a document-first workflow.

TLA+

Excels at modeling concurrent and distributed systems. Its model checker exhaustively explores a state space, and temporal operators let you express liveness and fairness properties directly.

Pantagruel has no temporal logic and cannot verify liveness or fairness—it checks safety properties only (invariant preservation, contradiction detection, precondition satisfiability). What it offers instead is a syntax designed to be read as a document: prose and formal statements are interleaved, so a specification can serve as its own explanation without a separate commentary.

Alloy

A relational modeling language whose Analyzer can find counterexamples automatically and visualize instances as graphs, making it excellent for exploring design spaces interactively.

Pantagruel also performs bounded checking via SMT, but has no instance visualizer and a narrower relational vocabulary. Its model is closer to classical pre/post specification: you declare domains, rules, and actions, and the checker verifies invariant preservation per action. The tradeoff is less exploratory power in exchange for a notation that reads like annotated prose.

Z Notation

A mature schema-based notation grounded in set theory and first-order logic. Widely used in safety-critical domains, with decades of tooling and pedagogy behind it.

Pantagruel borrows Z’s idea of structuring a specification around declared operations, state, and primed variables, but dispenses with the schema calculus and most of the mathematical notation. The result is less expressive but more approachable—meant for working programmers who want mechanical checking without learning a separate mathematical formalism.

Quick Start

Install from AUR

yay -S pantagruel

Install from Source (requires OCaml 4.14+ and opam)

Clone the repository:

git clone https://github.com/subsetpark/pantagruel.git

Install dependencies:

opam install . --deps-only

Build:

dune build

Install the pant application:

dune install

Learn More