> ## Asserting correctness

> Overview of assertions: expressing properties, the message parameter and language-specific implementations.

> Fetch the complete documentation index at: https://antithesis.com/docs/llms.txt
> Use this file to discover all available pages before exploring further.

---

## Assertions express properties

You express **properties** in Antithesis by adding **assertions** to your test harness and, (optionally) your code, using [one of our SDKs](/docs/reference/sdk/).

> **Important**
>
> Antithesis assertions (like everything in our SDKs) can run safely in production with minimal impact on your software’s performance.
>
> Unlike many assertion libraries, failed Antithesis assertions **do not cause your program to exit.** This lets you run the exact same code in test and production, and is useful in test, because we may be able to escalate an assertion failure into a more severe bug.

## 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](/docs/reference/sdk/).

## 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](/docs/product/understanding_test_results/reports/) 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](/docs/product/writing_tests/assertions/#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.*

> **Warning**
>
> If you change the `message` in a given assertion between test runs, you'll lose the history of that assertion. Conversely, if you retain the `message` but move the assertion, you'll still be able to track its history across runs (modulo the effects of your moving it).

## 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](/docs/introduction/how_antithesis_works/#the-antithesis-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](/docs/introduction/how_antithesis_works/#the-antithesis-multiverse), 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](/docs/product/writing_tests/instrumentation/coverage_instrumentation/) or [our SDK documentation](/docs/reference/sdk/) for details.

## Language-specific references

- [Go Assertions](https://antithesis.com/docs/generated/sdk/golang/assert/)
- [Java Assertions](https://antithesis.com/docs/generated/sdk/java/com/antithesis/sdk/Assert.html)
- [C++ Assertions](/docs/reference/sdk/cpp/assert/)
- [Python Assertions](https://antithesis.com/docs/generated/sdk/python/antithesis/assertions.html)
- [Rust Assertions](https://antithesis.com/docs/generated/sdk/rust/antithesis_sdk/assert/)
- [Languages not listed above](/docs/reference/sdk/fallback/assert/)
