A specification language checker for formal system descriptions.
Pantagruel lets you write precise specifications of systems using domains, rules, and logical propositions. The checker validates that your specifications are well-typed and internally consistent.
brew tap subsetpark/pantagruel https://github.com/subsetpark/pantagruel
brew install pantagruelRequires OCaml 4.14+ and opam.
# Install dependencies
opam install menhir sedlex ppx_deriving yojson sexplib0 parsexp alcotest
# Build
dune build
# Run tests
dune test
# Install globally (optional)
dune install# Type-check a specification file
pant myspec.pant
# Read from stdin
echo 'module TEST. Foo. ---' | pant
# Run bounded model checking (requires z3 or cvc5)
pant --check myspec.pant
pant --check --bound 5 myspec.pant # Set domain element bound (default: 3)
pant --check --solver cvc5 myspec.pant # Use alternative solver
# Output formats
pant --json myspec.pant # JSON with resolved types and full AST
pant --markdown myspec.pant # Rich Markdown with Unicode symbols
pant --format myspec.pant # Reformat with standard style
pant --normalize "root term" myspec.pant # Top-down normal form from root term
pant --ast myspec.pant # Print AST (OCaml format, for debugging)
# Specify module search path for imports
pant --module-path ./specs myspec.pantThe samples/ directory contains reference specifications:
01-basics.pant- Fundamental syntax: domains, rules, quantifiers02-library.pant- Library system with actions and state transitions03-types.pant- All type features: products, sums, lists, aliases04-operators.pant- All operators: logical, comparison, arithmetic05-state.pant- State transitions with primed expressions and frame conditions06-advanced.pant- Function overrides and qualified names07-pantagruel.pant- Self-specification of the Pantagruel language08-contexts.pant- Context declarations and write-permission boundaries09-closure.pant- Transitive closure declarations and acyclicity invariants10-cond.pant- Multi-armed conditional expressions with exhaustiveness checking
The samples/smt-examples/ directory demonstrates bounded model checking:
contradiction.pant- Conflicting postconditions detected by--checkinvariant-violation.pant- Missing precondition allows invariant violationdead-operation.pant- Unreachable action due to unsatisfiable preconditionunderspecified.pant- Well-specified banking example with contexts and frame conditions
A Pantagruel document consists of a module declaration, optional imports, and one or more chapters. Each chapter has a head (declarations) and a body (propositions), separated by ---.
module LIBRARY.
import USERS.
> Domains
Book.
Loan.
> Rules
available b: Book => Bool.
~> Borrow | u: User, b: Book.
---
> Propositions about the library
all b: Book | available b -> b in Book.
Domains define the basic types in your system:
User.
Document.
Type aliases create composite types:
Point = Nat * Nat. // Product type (tuple)
Result = Value + Error. // Sum type
UserList = [User]. // List type
Rules define operations with typed parameters:
// With return type
owner d: Document => User.
distance p: Point, q: Point => Real.
// Nullary (no parameters)
nobody => User.
Closures derive transitive closure rules from endorelations:
parent b: Block => Block + Nothing.
ancestor b: Block => [Block] = closure parent.
Actions define state transitions (no return type). Action labels are free-form text, separated from parameters by |:
// Action (with ~>) - for state transitions
~> Check out | u: User, d: Document.
~> Do something.
The body contains logical propositions that must be boolean:
// Literals
true.
false.
// Quantifiers
all u: User | u in User.
some d: Document | owner d = nobody.
// Comparisons
all x: Nat, y: Nat | x + y >= x.
// Membership and cardinality
all u: User | u in User.
#User >= 0.
Actions model state transitions. Within a chapter that has an action, you can use primed expressions to refer to the post-state of rules:
User.
Document.
owner d: Document => User.
~> Check out | u: User, d: Document.
---
// owner' refers to owner after check-out
owner' d = u.
Contexts define write-permission boundaries for actions. Context names are declared at the module level, and rules declare which contexts they belong to with a {Ctx} prefix. Actions specify which context they operate within using Ctx ~>.
module BANKING.
context Accounts.
Account.
{Accounts} balance a: Account => Nat.
Accounts ~> Withdraw | a: Account, amount: Nat.
---
balance' a = balance a - amount.
Multi-armed conditional expressions, where each arm is a boolean guard and each consequence has the same type:
// Classify priorities into tiers
all p: Priority | tier p = cond score p >= 100 => 3, score p >= 50 => 2, score p >= 10 => 1, true => 0.
Arms are checked left to right. When --check is used, the checker verifies that the arms are exhaustive — their disjunction covers all cases.
| Category | Operators |
|---|---|
| Logical | and, or, ~ (negation), -> (implication) |
| Comparison | =, !=, <, >, <=, >= |
| Membership | in, subset |
| Arithmetic | +, -, *, / |
| Other | # (cardinality), .N (projection), cond (conditional) |
// Line comment
> Doc comment (at start of line)
Bool- boolean valuesNat- positive integers (1, 2, 3, ...)Nat0- non-negative integers (0, 1, 2, ...)Int- all integersReal- real numbersString- text stringsNothing- empty/null type
Numeric types form a hierarchy: Nat < Nat0 < Int < Real
Specifications can import other modules:
module INVENTORY.
import PRODUCTS.
import WAREHOUSE.
Item.
stock i: Item => Nat0.
---
all i: Item | stock i >= 0.
Use --module-path to specify where to find imported .pant files.
module ACCOUNTS.
Account.
balance a: Account => Int.
~> Deposit | a: Account, amount: Nat.
---
// Balance increases after deposit
balance' a = balance a + amount.
// Other accounts unchanged
all other: Account | other != a -> balance' other = balance other.
module GEOMETRY.
Point = Real * Real.
origin => Point.
distance p: Point, q: Point => Real.
---
origin = (0.0, 0.0).
all p: Point | distance p p = 0.0.
all p: Point, q: Point | distance p q = distance q p.
The --check flag translates your specification into SMT-LIB2 and verifies it using an SMT solver (z3 by default). This performs checks at two levels.
Per-action checks. For each action, three checks are performed:
-
Contradiction detection - Are the action's postconditions satisfiable? If not, no state transition can satisfy all constraints simultaneously.
-
Invariant preservation - Do invariants (propositions in non-action chapters) still hold after the action fires? Reports a counterexample when a violation is found.
-
Precondition satisfiability - Can the action's preconditions ever be met, given the invariants? Flags unreachable "dead" operations.
Checking is bounded: domain types are modeled with a finite number of elements (default 3, configurable with --bound). The bound is automatically raised per domain when the specification declares more nullary constants of that domain type than the configured bound (e.g., 5 named constants of type Color will use bound 5 for Color even if --bound 3). This means checks are sound within the bound but not complete for all possible domain sizes.
Cond exhaustiveness. Every cond expression in the document is checked for exhaustiveness: the solver verifies that the disjunction of all arm conditions is always true (within the enclosing quantifier context). A non-exhaustive cond reports a counterexample showing variable assignments where no arm is true.
Guard-aware verification. Declaration guards (e.g., score u: User, active u => Nat.) are automatically injected as antecedents in SMT queries. When a quantified proposition applies a guarded function, the guard is threaded into the quantifier's condition. This prevents false positives from the solver applying functions outside their declared domain.
module BANKING.
context Accounts.
Account.
{Accounts} balance a: Account => Nat0.
---
all a: Account | balance a >= 0.
where
Accounts ~> Withdraw | a: Account, amount: Nat.
---
balance' a = balance a - amount.
all b: Account | b != a -> balance' b = balance b.
$ pant --check banking.pant
OK: Action 'Withdraw' postconditions are satisfiable
FAIL: Invariant 'all a: Account | balance a >= 0' may be violated by action 'Withdraw'
Action:
a = Account_0
amount = 2
Before:
balance Account_0 = 1
After:
balance' Account_0 = -1
OK: Action 'Withdraw' preconditions are satisfiableThe counterexample shows that withdrawing 2 from a balance of 1 violates the non-negative invariant. The fix is to add a precondition: balance a >= amount.
When an action declares a context (Accounts ~> Withdraw), the checker automatically generates frame conditions: functions not in the context are asserted unchanged. This means invariants that only reference extracontextual functions are trivially preserved and skipped, reducing verification work.
Pantagruel can be used with any editor that supports LSP through efm-langserver.
Add to your efm-langserver config (typically ~/.config/efm-langserver/config.yaml):
version: 2
tools:
pantagruel-lint: &pantagruel-lint
lint-command: 'pant ${INPUT}'
lint-stdin: false
lint-formats:
- '%f:%l:%c: error: %m'
languages:
pantagruel:
- <<: *pantagruel-lintrequire('lspconfig').efm.setup({
filetypes = { 'pantagruel' },
init_options = { documentFormatting = true },
})
-- Associate .pant files with pantagruel filetype
vim.filetype.add({
extension = { pant = 'pantagruel' }
})Install the efm-langserver extension and configure similarly.
BSD-3