Asserting correctness

Assertions express properties

You express properties in Antithesis by adding assertions to your test harness and, (optionally) your code, using one of our SDKs.

Types of assertions

Antithesis provides 4 types of assertions:

always(...) assertions: Assert that a condition is reached at least once and must hold every time this assertion is evaluated. A single false evaluation fails the property.
alwaysOrUnreachable(...) assertions: Assert that a condition must hold every time it is reached, but also evaluate “not encountered” as passing. This is useful for checks in optional or rare paths.
reachable() and unreachable() assertions: Assert pure reachability properties. reachable() means “this location should be hit at least once” per test run; unreachable() means “this location should never be hit.”
sometimes(...) assertions: Assert that a condition should be true at least once per test run. These are especially useful for checking whether tests exercise meaningful scenarios, not just particular pieces of code.

The exact function names differ by language, but these conceptual categories are consistent across all our SDKs.

The `message` parameter

You add assertions to your test harness, but what you care about, and what Antithesis displays in test results, are system properties.

Assertions aggregate to properties via the message parameter.

All Antithesis assertions require a message parameter, which appears in the triage report as the name of a property. We strongly recommend that message be a human-readable description of the property being checked.

We encounter each assertion many times during a single Antithesis test run, so whether the property holds depends on the whole body of encounters. For more detail on this, see evaluating assertions below.

For example, each of the “Control service” properties in the example below is a message in an assertion.

Antithesis generates one property per unique message. If you have multiple assertions with the same message, Antithesis evaluates all those encounters as one body.

Evaluating assertions

Antithesis evaluates each assertion as it’s encountered at runtime, to see if the assertion holds in that moment. When an assertion is encountered, it sends a JSONL message to Antithesis indicating whether the encounter passed or failed.

Antithesis then analyzes the whole body of encounters with all assertions that share a message across an entire multiverse to determine whether the property passes or fails. Exactly how this is done varies depending on the type of assertion.

Always assertions

Always assertions are disproved by a single failing encounter, but cannot be proved with perfect certainty by any number of passing encounters.
Therefore, failing encounters are more important than passing ones, and
Always assertions are listed as passing by default until disproved by a failing encounter or if there no encounters at all.

Sometimes assertions

Sometimes assertions are proved by a single passing encounter, but cannot be disproved with perfect certainty by any number of failing encounters.
Therefore, passing encounters are more important than failing ones, and
Sometimes assertions are listed as failing by default until proven by a passing encounter.

Reachability assertions

Reachability assertions are disproved when there are no encounters.
If there are no encounters during the test run, the assertion fails.

Unreachability assertions

These are opposite of reachability assertions and are disproved by a single passing encounter.
If there’s at least one passing encounter during the test run, the assertion fails.

Assertions are clues

Assertions also provide hints to our platform about which states should be explored in order to search for bugs. This is an important form of guidance for our platform and makes its exploration of your software much more efficient.

Using assertions ensures you get the best bang for your buck in Antithesis.

Assertion cataloging

When you start a test run, Antithesis initializes and catalogs every assertion in all your containers. At this time, each assertion send a JSONL message declaring itself to Antithesis.

Remember that in any given execution history, Antithesis may not encounter every assertion you make. Since some types of assertions are supposed to fail if they’re never reached, Antithesis must be informed that that these assertions exist so it can mark them as failing when this happens.

Our SDKs handle assertion cataloging for you, though the precise way this happens differs from language to language. Please read instrumentation or our SDK documentation for details.