PropEr makes Erlang code prove properties instead of enumerating cases

Why enumerating test cases is the wrong shape for Erlang

The README starts with the traditional method and its two problems, and they are the reason this tool exists. Traditional testing involves writing a series of test inputs along with their corresponding expected outputs, then running the program with those inputs and observing whether it behaves as expected. It is simple and easy to automate, but writing test cases by hand is tedious and time consuming, and it is hard to know whether the test suite covers all aspects of the software under test. Property-based testing inverts that. The tester specifies only the generic structure of valid inputs for the program under test, plus the properties about the program's behaviour and the input-output relation that are expected to hold for every valid input. The tool then randomly produces progressively more complex valid inputs, applies them to the program while monitoring its execution, and checks that it behaves according to the supplied properties. The examples in the README are ordinary properties written in plain language. A program should accept any character string and convert all lowercase letters inside the string to uppercase. A program should accept any list of integers, and if the input list is at least four elements long it should return the fourth largest integer, otherwise it should throw an exception. Read that second example carefully. It states the domain, the behaviour and the boundary condition in one sentence, and it has no enumerated inputs at all. That is the entire value proposition. The audience is Erlang developers, and the focus is on the behaviour of pure functions, with a separate subsystem for stateful code on top.

Generators built from the Erlang type language

The part that makes PropEr more than a generic random data generator is its integration with Erlang's own type language. The README lists three consequences of that integration. Types expressed in the Erlang type language can be used instead of generators written in PropEr's own type system as input data specifications. Generators for abstract data types can be constructed automatically using the ADTs' API functions. And PropEr can test functions automatically, based solely on information provided in their specs. That third point is the strongest one and deserves unpacking. If a function already has a spec that describes what it accepts, PropEr can use those specs to drive the testing rather than requiring you to restate the domain in a second notation. For a code base that is disciplined about specs, that removes most of the work of writing a property test. The properties themselves are written as ordinary Erlang expressions, with the help of a few predefined macros, and the input domain of functions is specified through the use of a type system modelled closely after the type system of the language itself. For algebraic data types, the automatic construction of generators from the API functions means the test data matches the shape the type intends, including the recursive structures that hand written generators usually get wrong. The repository's examples directory shows the range in practice, with files for an ADT based stack, a labyrinth, a mastermind style game, a base64 example, and several that are explicitly state machines, among them car_fsm.erl, elevator_fsm.erl, ets_statem.erl and pdict_statem.erl.

Stateful code gets its own subsystem

Property-based testing of pure functions is the easy half. The README notes that on top of its focus on pure functions, PropEr is equipped with two library modules that can be used for testing stateful code. That is the hard half, because a stateful system needs a model of its expected behaviour to compare against, and it needs the sequence of operations to be generated rather than the final state to be checked in isolation. The examples directory is heavy on state machine cases for that reason. The car_fsm.erl, elevator_fsm.erl, ets_statem.erl and pdict_statem.erl examples cover different flavours of stateful behaviour, from a car whose gear and speed evolve to a system built on ETS tables and one built on the process dictionary. This is where the original authors split the work. The README credits the base PropEr system as written mainly by Manolis Papadakis, and the stateful code testing subsystem to Eirini Arvaniti, with Kostis Sagonas actively maintaining the code base since 2012. The copyright line reads 2010-2026 by Manolis Papadakis, Eirini Arvaniti, and Kostis Sagonas, which puts the age of the project at well over a decade. That is worth knowing when you are choosing a testing tool, because it means the generator library has been shaped by a lot of real Erlang.

Building it and putting it on the Erlang library path

The quickstart is a set of small steps. First get the sources, either a tagged version from the Tags list on GitHub or a clone of the current code base.

git clone [email protected]:proper-testing/proper.git

Then compile. Simply running make builds PropEr. If you intend to change the code or submit a pull request, the README says you most likely want make test to run the unit tests and make dialyzer to also run dialyzer on the code base. To do both and build the documentation, issue a make all, which additionally needs the syntax_tools application and a recent version of EDoc. There is also a Homebrew route.

brew install proper

Then the library path. The README gives two methods, the ERL_LIBS environment variable in your shell startup file.

export ERL_LIBS=/full/path/to/proper

or a line in your .erlang resource file.

code:load_abs("/full/path/to/proper").

After that you add the include line to all source files that contain properties.

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

and compile those source files, preferably with debug_info enabled. The Makefile shows how the build actually works. The default target is compile, which uses rebar3 and then symlinks the built ebin directory, and the all target is compile dialyzer doc test. The rebar3 version is pinned to 3.15.2, with a comment explaining that this is a safe version that still supports Erlang/OTP 20.x and 21.x and should be upgraded when support for those versions is dropped. There is also a rebar.config and a rebar.cmd for Windows.

Running one property, and the EUnit clash you will hit

A property is a function, and running it is one call.

proper:quickcheck(your_module:some_property()).

That is the whole interface for the common case. The README points at the tutorials and testing tips on the project's home page for getting started, and notes that the API documentation can be built from source with make doc. If you run properties from EUnit, two specific problems come up, and the README documents both. The first is a macro name collision. Both systems define a ?LET macro, and the fix is to include PropEr's header file before EUnit's, so that any instance of ?LET counts as a PropEr ?LET. The second is that EUnit captures standard output, so PropEr output is normally not visible when proper:quickcheck() is invoked from EUnit. The workaround is to pass the option {to_file, user}.

?assertEqual(true, proper:quickcheck(your_mod:some_prop(), [{to_file, user}])).

That makes PropEr properties visible even when invoked from EUnit, which matters because a property that fails quietly inside an EUnit run is worse than no test at all. The README also has a section on incompatibilities with QuviQ's QuickCheck, stating that PropEr's notation and output format has been kept quite similar. That comparison is the closest thing to an alternative in the documentation, and the difference is that PropEr is Erlang native, integrates with the Erlang type language, and is GPL licensed rather than commercial.

GPL version 3, a slow release cadence, and a still active project

The licence is GPL version 3 or later, as the README states and as the COPYING file at the root of the tree carries. The Makefile header repeats the terms, including the standard notice about the warranty. That is the single most consequential fact for an adopter outside the open source world. A permissive licence would let you use PropEr inside a proprietary product without ceremony. The GPL means that distributing a work linked to PropEr carries obligations, and that is a question for your legal counsel rather than for this article. The README also notes that PropEr is available on Hex PM, with a badge for it. On activity, the last push was on 2026-06-24 and the repository is not archived, so work continues. The releases are v1.5.0 from 2025-03-26, v1.4 from 2021-05-18 and v1.3 from 2018-07-25, so the current release line is a slow one, which is normal for a testing library whose API has been stable for years. The repository layout supports the development story. There is src/ for the code, test/ for the unit tests, examples/ for the reference properties, include/ for the header, doc/ for the documentation, scripts/, a .plt/ directory for the dialyzer base PLT, and a THANKS file. The dialyzer setup is worth one more look, because it is a quality practice that many Erlang projects skip. The dialyzer target depends on .plt/proper_plt and runs dialyzer with -Wunmatched_returns over the compiled ebin, so unmatched return values are treated as warnings in the project's own build.

Editorial conclusion

Adopt PropEr when you are writing Erlang and want to test a pure function or a state machine by stating what must always hold rather than by hand writing input and expected output pairs. Do not adopt it for property-based testing in another language, since the generators and the type integration are Erlang specific. Before you start, check that your build can run dialyzer and that you can include the PropEr header, and note that the tool is GPL version 3 or later, so linking it into a proprietary product needs a licence review.

Frequently asked questions

Official sources

1. License: GPL-3.0
2. Project website
3. proper-testing/proper on GitHub
4. README
5. Releases