Layer 1: invariants and properties on a running OTP process, checked at every transition.

defmodule Account do
  use GenServer
  use ExTLA.Invariant

  invariant :never_negative, desc: "an account may not go below zero" do
    state.balance >= 0
  end

  action_property :no_free_money do
    new.balance <= old.balance or new.deposits > old.deposits
  end

  precondition {:withdraw, amount} do
    amount > 0
  end
end

state is bound in an invariant, old and new in an action_property, and in a precondition or postcondition the pattern's own bindings are in scope alongside them. Nothing is passed in explicitly, because a property is a statement about the process rather than a function of arguments.

defoverridable and super, not renaming

The @before_compile hook wraps each callback the module defines by marking it overridable and defining a new one that calls super, rather than renaming the original. Every real GenServer has several handle_call/3 clauses with guards; renaming would have to reproduce every clause head and its guards exactly, and any mistake silently changes dispatch. super keeps the original clauses intact and dispatches to them with their own pattern matching.

use ExTLA.Invariant goes directly after use GenServer and before the callbacks, and the order is load-bearing rather than stylistic. Only the callbacks the module's own author writes are wrapped, and they are identified with @on_definition, which sees a definition only after it is installed. That is what keeps the wrapper off the default handle_call/3, handle_cast/2 and handle_info/2 that use GenServer injects — Module.defines?/2 cannot tell those from the author's, calling super on them is deprecated, and wrapping a default that exists to stop the server with a :bad_call is checking a transition nobody wrote.

init/1 is the exception, and it needs a second guard. GenServer injects it from its own @before_compile, which runs after the hook is installed rather than before — so @on_definition does see it, and {:init, 1} lands in the wrapped set for a module whose author wrote no init/1. By then GenServer's defoverridable init: 1 has moved it out of the definitions table, and Module.make_overridable/2 refuses:

** (ArgumentError) cannot make function init/1 overridable because it was not defined

naming neither this library nor the cause — for a module as plain as the example at the top of this moduledoc. So the wrapper is emitted only for a callback still in the definitions table when __before_compile__/1 runs — which is precisely what make_overridable/2 requires, asked as a question rather than assumed.

:disabled emits nothing

When ExTLA.Config.mode/0 resolves to :disabled where the module compiles, the hook emits no wrapper and no defoverridable, and the module compiles exactly as written. That is what "zero production cost" has to mean: not cheap emitted code, but none. It is also why the mode is a compile_env macro — a runtime lookup would leave an Application.get_env/2 call and a branch on every callback, which alone would exceed the budget the whole layer is meant to fit in.

Cost is decided at compile time wherever it can be

callbacks: restricts an invariant to particular callbacks, and the restriction is resolved when the wrapper is generated. A hot callback in a module with nine invariants emits a call naming the two that apply, rather than nine names and a filter. Where a callback ends up with nothing to check, no call is emitted for it at all.

enabled: false is evaluated at compile time and emits nothing anywhere, for a check too costly to run outside a particular environment.