> ## Properties in Antithesis

> Always and sometimes properties, default and custom properties, and how Antithesis analyses properties.

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

---

This section explains how Antithesis analyzes the properties you define. To understand how to express these properties in your software, see [Assertions in Antithesis](/docs/concepts/properties_assertions/assertions/).

For a discussion of what kinds of properties you might want to specify and why, see [Properties to Test For](/docs/concepts/properties_assertions/reliability_properties/). We also publish property catalogs for different system shapes. We have catalogs for [blockchains](/docs/resources/blockchain_property_catalog/) and [key-value datastores](/docs/resources/kv_property_catalog/).

If you're working with a coding agent, we offer [an agent skill](https://github.com/antithesishq/antithesis-skills/tree/main/antithesis-research) that analyzes your system and generates a basic property catalog based on your system architecture, which may serve as a useful starting point.

## Defining properties

What kinds of assurances or promises have you made to your users? Common promises -- often implicit -- include things like: the application will recover after a single node dies, or the database will eventually be consistent, or that the system will never run out of memory. Nearly any such promise can usefully be asserted as a property for Antithesis to test.

A small number of properties can provide a very large amount of test coverage, because each of them has the potential to catch many different, unrelated bugs.

For example, suppose you have a unit test that does the following:

1. It takes a list with one element,
2. Then pushes two elements onto the list,
3. Then pops three elements off the list,
4. And finally asserts that the list is empty.

While this could be written as-is as a test in Antithesis, you're really attempting to verify a specific case of this more general property:

```bash
always(
  ending length of list = starting length + number of pushes - number of pulls
)
```

So it's more effective to assert this more general and abstract property directly, then create a randomized [test template](/docs/product/test_templates/) and see if it's always true. Asserting your existing unit tests as properties in Antithesis can actually be a good way to get started, because Antithesis will check whether they still work under [fault injection](/docs/concepts/fault_injection/) and other environmental variation.

### Default and Custom properties

Antithesis comes with a large set of **default properties**, which are applicable to nearly every piece of software. These properties include: never running out of memory, never crashing, never emitting certain sorts of errors and so on. These are preconfigured for you in our system.

Antithesis also enables you to define **custom properties** specific to your system. For instance, "the system will be availabile if a single node is killed" is a property that's not as universal as "never crashing," and is easily expressed [using our SDKs](/docs/reference/sdk/).

### Always and Sometimes properties

Antithesis classifies properties as **always properties** or **sometimes properties**.

*Always properties* assert that something is always (or never) the case. The kind of assertions you might already use to specify expected code behavior are examples of *always properties:* that certain lists will be non-empty, that certain parameters will be positive numbers, and so on.

*Sometimes properties* assert that something will happen *at least once* during a testing session. These are a better alternative to code coverage: not only can you assert that particular sections of your code are sometimes exercised, you can also assert that functions are sometimes called with certain parameters (such as negative values), or that you sometimes see one event before another (such as a leader election before a rollback).

*Sometimes properties* are so important that they get [a whole section to themselves](/docs/concepts/properties_assertions/sometimes_assertions/).

## How Antithesis analyzes properties

### Examples and counterexamples

During a testing session, Antithesis evaluates each [assertion](/docs/concepts/properties_assertions/assertions/) encountered in [each execution history](/docs/product/debugging/advanced_multiverse_debugging/moment_branch/) to see whether the properties you asserted were true or false. This generates **examples** and **counterexamples** for each property: moments consistent with the property being true, or false.

### Passing and failing

When Antithesis finishes a testing session, it decides whether each property **passed** or **failed,** and summarizes those findings in the [triage report](/docs/product/reports/). Here the treatment of *always properties* and *sometimes properties* differs.

#### Always properties

You might specify as an *always property* that "the system should never crash." Any moment when the system doesn't crash is an example of that property, whereas any crash is a counterexample.

- *Always properties* are disproved by a single counterexample, but cannot be proved with perfect certainty by any number of examples.
- Therefore, counterexamples are more important than examples, and
- *Always properties* are listed as passing by default until disproved by a counterexample.

#### Sometimes properties

You might specify as a *sometimes property* that "the system will sometimes see rollbacks." Any rollback is an example of that property, whereas moments without rollbacks are counterexamples.

- *Sometimes properties* are proved by a single example, but cannot be disproved with perfect certainty by any number of counterexamples.
- Therefore, examples are more important than counterexamples, and
- *Sometimes properties* are listed as failing by default until proven by an example.
