Declare @pre/@post contracts on a behaviour's @callbacks and have them enforced on every implementing module.

This is where Design by Contract meets the Liskov Substitution Principle: a behaviour is a promise about a family of implementations, and a contract is the formal content of that promise. A module that use Bond.Behaviour attaches contracts to its callbacks; a module that use Bond, behaviours: [TheBehaviour] inherits and enforces those contracts on its own clauses.

defmodule Ledger do
  use Bond.Behaviour

  @pre positive_amount: amount > 0
  @post non_negative: result >= 0
  @callback withdraw(balance :: non_neg_integer, amount :: pos_integer) :: non_neg_integer
end

defmodule BankAccount do
  use Bond, behaviours: [Ledger]

  @impl true
  def withdraw(balance, amount) when amount <= balance, do: balance - amount
end

A @pre/@post precedes the @callback it attaches to, exactly as a contract precedes the def it attaches to in use Bond. The contract expressions reference the callback's argument names (balance, amount above); those names become canonical, and an implementation's parameters are rebound to them positionally — so the impl is free to name its parameters differently.

Immutable inheritance (v1)

Inherited contracts are immutable: an implementation may not weaken, strengthen, or add to them. Attaching @pre/@post to an impl function whose {name, arity} matches an inherited contract is a compile error — use Bond.check/1 in the body for implementation-specific assertions. Forbidding (rather than silently accepting) impl-level contracts on inherited operations keeps that syntax reserved for a future Eiffel-style refinement feature (@pre_else/@post_then).

Reflection

use Bond.Behaviour generates a __bond_contracts__/0 function on the behaviour module that returns its callback contracts keyed by {name, arity}. It is an internal reflection hook read by use Bond, behaviours: […] at the implementer's compile time; you should not call it directly.