PropEr: Property-Based Testing for Erlang and Elixir Deep Dive

HelpMeTest

19 Aug 2026 — 6 min read

PropEr is the open-source property-based testing library for Erlang, directly inspired by Quviq's commercial QuickCheck. It brings full stateful testing, type-based generation, and targeted property-based testing (TPBT) to the Erlang/OTP ecosystem. For Elixir, PropEr integrates with ExUnit via the PropCheck library.

Why PropEr for Erlang Systems

Erlang's actor model and OTP behaviors (gen_server, gen_statem, supervisor) are stateful by nature. PropEr's statem module is designed specifically for this: it models OTP process state and generates call sequences that expose protocol violations.

Generator Types and Macros

PropEr uses macros for generators, which is syntactically different from Haskell/Python approaches:

-module(prop_basic).
-include_lib("proper/include/proper.hrl").

%% Generate a positive integer
prop_positive() ->
    ?FORALL(N, pos_integer(),
        N > 0).

%% Generate a non-empty list
prop_non_empty_list() ->
    ?FORALL(Xs, non_empty(list(integer())),
        length(Xs) > 0).

%% Frequency-controlled generation
day_of_week() ->
    frequency([
        {5, weekday()},
        {2, weekend()}
    ]).

weekday() ->
    oneof([monday, tuesday, wednesday, thursday, friday]).

weekend() ->
    oneof([saturday, sunday]).

Custom Generator Combinators

%% Generate a valid email address
email() ->
    ?LET({User, Domain, Tld},
         {non_empty(list(oneof([range($a, $z), range($0, $9)]))),
          non_empty(list(range($a, $z))),
          oneof(["com", "org", "net", "io"])},
         list_to_binary([User, $@, Domain, $., Tld])).

%% Generate a valid HTTP status code
http_status() ->
    oneof([200, 201, 204, 301, 302, 400, 401, 403, 404, 422, 500, 503]).

%% Generate a request with method-appropriate body
http_request() ->
    ?LET(Method, oneof([get, post, put, delete, patch]),
         case Method of
             M when M =:= post; M =:= put; M =:= patch ->
                 ?LET(Body, json_object(),
                      #{method => Method, body => Body});
             _ ->
                 #{method => Method, body => null}
         end).

json_object() ->
    ?LET(Pairs, list({non_empty(binary()), json_value()}),
         maps:from_list(Pairs)).

json_value() ->
    oneof([
        integer(),
        float(),
        binary(),
        boolean(),
        null
    ]).

Type-Based Generation

PropEr can generate values directly from Erlang type specifications:

-type user_id() :: pos_integer().
-type email()   :: binary().
-type role()    :: admin | user | guest.

-record(user, {
    id    :: user_id(),
    email :: email(),
    role  :: role()
}).

%% PropEr generates User records from the type spec
prop_user_creation() ->
    ?FORALL(User, #user{},
        begin
            Result = user_db:create(User),
            case Result of
                {ok, _Id} -> true;
                {error, _} -> true  % We care about no crashes, not success
            end
        end).

Use proper_types:exactly/1 for precise type matching:

-spec create_user(user_id(), email(), role()) -> {ok, user_id()} | {error, term()}.

PropEr generates inputs matching these specs automatically when you use ?FORALL with type-derived generators.

Shrinking in PropEr

PropEr shrinking works via generator-based shrinking—each generator knows how to shrink its output:

%% Custom type with custom shrinker
-type sorted_list() :: [integer()].

sorted_list_gen() ->
    ?LET(Xs, list(integer()), lists:sort(Xs)).

%% The shrinking of sorted_list() automatically maintains sortedness
%% because it shrinks the underlying list and re-sorts

prop_sorted_property() ->
    ?FORALL(Xs, sorted_list_gen(),
        begin
            Sorted = lists:sort(Xs),
            Sorted =:= Xs
        end).

For custom shrinking behavior, use ?SHRINK:

%% Shrink a binary by removing bytes from the end
shrinkable_binary() ->
    ?SHRINK(
        binary(),
        [binary(max(0, byte_size(B) - 1)) || B <- [binary()]]
    ).

Stateful Testing with `proper_statem`

This is PropEr's most powerful feature for Erlang: testing OTP gen_servers.

Testing a gen_server

-module(prop_account_server).
-behaviour(proper_statem).
-include_lib("proper/include/proper.hrl").
-export([
    initial_state/0,
    command/1,
    precondition/2,
    postcondition/3,
    next_state/3
]).

%% Model state
-record(state, {
    accounts = #{} :: #{binary() => integer()}
}).

%% Initial model state
initial_state() -> #state{}.

%% Command generation
command(#state{accounts = Accounts}) ->
    AccountIds = maps:keys(Accounts),
    frequency(
        [{5, {call, account_server, create_account, [binary(), pos_integer()]}}] ++
        case AccountIds of
            [] -> [];
            _  -> [
                {3, {call, account_server, deposit,
                     [oneof(AccountIds), pos_integer()]}},
                {3, {call, account_server, withdraw,
                     [oneof(AccountIds), pos_integer()]}},
                {2, {call, account_server, get_balance,
                     [oneof(AccountIds)]}},
                {1, {call, account_server, close_account,
                     [oneof(AccountIds)]}}
            ]
        end
    ).

%% Preconditions
precondition(State, {call, _, withdraw, [Id, Amount]}) ->
    case maps:get(Id, State#state.accounts, undefined) of
        Balance when is_integer(Balance), Balance >= Amount -> true;
        _ -> false
    end;
precondition(State, {call, _, deposit, [Id, _]}) ->
    maps:is_key(Id, State#state.accounts);
precondition(State, {call, _, get_balance, [Id]}) ->
    maps:is_key(Id, State#state.accounts);
precondition(State, {call, _, close_account, [Id]}) ->
    maps:is_key(Id, State#state.accounts);
precondition(_, _) ->
    true.

%% State transitions (model)
next_state(State, _Result, {call, _, create_account, [Id, Initial]}) ->
    State#state{accounts = maps:put(Id, Initial, State#state.accounts)};
next_state(State, _Result, {call, _, deposit, [Id, Amount]}) ->
    Accounts = maps:update_with(Id, fun(B) -> B + Amount end, State#state.accounts),
    State#state{accounts = Accounts};
next_state(State, _Result, {call, _, withdraw, [Id, Amount]}) ->
    Accounts = maps:update_with(Id, fun(B) -> B - Amount end, State#state.accounts),
    State#state{accounts = Accounts};
next_state(State, _Result, {call, _, close_account, [Id]}) ->
    State#state{accounts = maps:remove(Id, State#state.accounts)};
next_state(State, _, _) ->
    State.

%% Postconditions
postcondition(State, {call, _, get_balance, [Id]}, Result) ->
    maps:get(Id, State#state.accounts) =:= Result;
postcondition(_, {call, _, create_account, _}, Result) ->
    Result =:= ok;
postcondition(_, _, _) ->
    true.

%% The actual property
prop_account_server() ->
    ?FORALL(Cmds, commands(?MODULE),
        begin
            {ok, _Pid} = account_server:start_link(),
            {History, State, Result} = run_commands(?MODULE, Cmds),
            account_server:stop(),
            ?WHENFAIL(
                io:format("History: ~p~nState: ~p~nResult: ~p~n",
                          [History, State, Result]),
                aggregate(command_names(Cmds), Result =:= ok)
            )
        end).

Testing Concurrent gen_servers with `parallel_commands`

prop_account_parallel() ->
    ?FORALL(Cmds, parallel_commands(?MODULE),
        begin
            {ok, _Pid} = account_server:start_link(),
            {Seq, Par, Result} = run_parallel_commands(?MODULE, Cmds),
            account_server:stop(),
            ?WHENFAIL(
                io:format("Seq: ~p~nPar: ~p~nResult: ~p~n", [Seq, Par, Result]),
                Result =:= ok
            )
        end).

parallel_commands/1 generates a sequential prefix followed by concurrent command groups. PropEr checks that all interleavings produce results consistent with some sequential execution (linearizability). This finds race conditions in gen_server implementations.

Targeted Property-Based Testing (TPBT)

PropEr's unique feature: directed search using simulated annealing. Instead of random generation, TPBT guides the search toward inputs that maximize a utility function.

%% Find inputs that maximize cache miss rate
prop_cache_performance() ->
    ?FORALL_TARGETED(Sequence, list(integer()),
        begin
            CacheMisses = simulate_cache(Sequence),
            ?MAXIMIZE(CacheMisses),
            true  % We're maximizing, not asserting failure
        end).

%% Find inputs that trigger timeout in a parser
prop_parser_no_timeout() ->
    ?FORALL_TARGETED(Input, binary(),
        begin
            Start = erlang:system_time(millisecond),
            parse(Input),
            Duration = erlang:system_time(millisecond) - Start,
            ?MAXIMIZE(Duration),
            Duration < 1000  % Fails if we find input taking > 1s
        end).

TPBT is particularly useful for:

Performance testing: find worst-case inputs
Security testing: maximize complexity metrics to find algorithmic complexity attacks
Fuzz testing: guide toward code paths that are rarely hit by random inputs

PropEr with Elixir (PropCheck)

The PropCheck library wraps PropEr for Elixir/ExUnit:

defmodule AccountTest do
  use ExUnit.Case
  use PropCheck

  property "deposit increases balance" do
    forall {initial, amount} <- {pos_integer(), pos_integer()} do
      account = Account.new(initial)
      updated = Account.deposit(account, amount)
      Account.balance(updated) == initial + amount
    end
  end

  property "withdraw cannot exceed balance" do
    forall {initial, attempt} <- {pos_integer(), pos_integer()} do
      account = Account.new(initial)
      case Account.withdraw(account, attempt) do
        {:ok, updated}   -> Account.balance(updated) == initial - attempt
        {:error, :insufficient_funds} -> attempt > initial
      end
    end
  end
end

Elixir Stateful Testing with PropCheck

defmodule QueueStateMachine do
  use PropCheck.StateM

  # Model state: a simple list
  def initial_state, do: []

  # Command generation
  def command(state) do
    always_possible = [
      {:call, MyQueue, :new, []},
      {:call, MyQueue, :push, [term()]}
    ]
    
    when_has_items = if state == [], do: [], else: [
      {:call, MyQueue, :pop, []},
      {:call, MyQueue, :peek, []}
    ]
    
    frequency(
      [{3, cmd} | Enum.map(when_has_items, &{2, &1})]
      |> List.flatten()
    )
  end

  # State transitions
  def next_state(state, _result, {:call, _, :push, [item]}) do
    state ++ [item]
  end

  def next_state([_head | tail], _result, {:call, _, :pop, []}) do
    tail
  end

  def next_state(state, _, _), do: state

  # Postconditions
  def postcondition([head | _], {:call, _, :peek, []}, result) do
    result == head
  end

  def postcondition([head | _], {:call, _, :pop, []}, result) do
    result == {:ok, head}
  end

  def postcondition([], {:call, _, :pop, []}, result) do
    result == {:error, :empty}
  end

  def postcondition(_, _, _), do: true
end

defmodule QueueTest do
  use ExUnit.Case
  use PropCheck
  use PropCheck.StateM

  property "queue behaves correctly" do
    forall cmds <- QueueStateMachine.commands() do
      {_history, _state, result} = QueueStateMachine.run_commands(cmds)
      result == :ok
    end
  end
end

Integrating PropEr with rebar3

%% rebar.config
{profiles, [
    {test, [
        {deps, [
            {proper, "1.4.0"}
        ]},
        {erl_opts, [debug_info]}
    ]}
]}.

{proper_opts, [
    {numtests, 1000},
    {max_shrinks, 200}
]}.

Run:

rebar3 proper          # Run all prop_ prefixed functions
rebar3 proper --module prop_account  # Run specific module
rebar3 proper --prop prop_account_server  # Run specific property

Reproduce a failure:

prop_account_server: Failed! After 17 tests.
Counterexample: [...]
--> Shrinking .....(5 times) 
[{set,{var,1},{call,account_server,create_account,[<<"user1">>,100]}},
 {set,{var,2},{call,account_server,withdraw,[<<"user1">>,50]}},
 {set,{var,3},{call,account_server,withdraw,[<<"user1">>,60]}}]

Replay:

rebar3 proper --prop prop_account_server --noshrinker

Key Takeaways

?FORALL macro is the entry point—generates random inputs matching a type
frequency/1 controls distribution to match realistic call patterns
proper_statem models OTP gen_server state and generates call sequences—essential for finding Erlang process bugs
parallel_commands/1 verifies linearizability for concurrent gen_server access
Targeted PBT (?FORALL_TARGETED, ?MAXIMIZE) guides search toward worst-case inputs
PropCheck brings full PropEr capabilities to Elixir/ExUnit
Type-derived generation uses -spec annotations to generate valid inputs automatically

PropEr's statem testing is particularly well-suited to Erlang because OTP gen_servers are natural state machines. The parallel commands feature catches race conditions that are otherwise extremely difficult to test—and in production Erlang systems, those concurrency bugs are exactly the ones that matter most.

PropEr: Property-Based Testing for Erlang and Elixir Deep Dive

HelpMeTest

Why PropEr for Erlang Systems

Generator Types and Macros

Custom Generator Combinators

Type-Based Generation

Shrinking in PropEr

Stateful Testing with `proper_statem`

Testing a gen_server

Testing Concurrent gen_servers with `parallel_commands`

Targeted Property-Based Testing (TPBT)

PropEr with Elixir (PropCheck)

Elixir Stateful Testing with PropCheck

Integrating PropEr with rebar3

Key Takeaways

Read more

Test Result Reporting and Failing Fast in CI Pipelines

SOC 2 Evidence Collection Automation: Stop Emailing Screenshots to Your Auditor

PCI-DSS 4.0 Penetration Testing: Scoping, Methodology, and What Assessors Actually Check

Data Pipeline CI/CD Testing: Automate Quality Gates

Why PropEr for Erlang Systems

Generator Types and Macros

Custom Generator Combinators

Type-Based Generation

Shrinking in PropEr

Stateful Testing with proper_statem

Testing a gen_server

Testing Concurrent gen_servers with parallel_commands

Targeted Property-Based Testing (TPBT)

PropEr with Elixir (PropCheck)

Elixir Stateful Testing with PropCheck

Integrating PropEr with rebar3

Key Takeaways

Read more

Test Result Reporting and Failing Fast in CI Pipelines

SOC 2 Evidence Collection Automation: Stop Emailing Screenshots to Your Auditor

PCI-DSS 4.0 Penetration Testing: Scoping, Methodology, and What Assessors Actually Check

Data Pipeline CI/CD Testing: Automate Quality Gates

Stateful Testing with `proper_statem`

Testing Concurrent gen_servers with `parallel_commands`