# Invariants

Invariants shape how the solver looks for a viable solution. They are statements that are either assumed to be true or that we want the solver to disprove.

## Temporal Logic

Fault has a couple of temporal logic operators that create SMT rules to test conditions across time. Fault is not as good at temporal logic as other languages specifically designed for it (TLA+ comes to mind), but it can handle some basic reasoning.

Operator | Definition | Use |
---|---|---|

`eventually` | At some point in the model runtime this assertion will be true | `assert x eventually;` |

`always` | This assertion is always true (technically the default for all assertions) | `assert x always;` |

`eventually-always` | When this assertion becomes true it will stay true for the rest of the model runtime | `assert x eventually-always;` |

`nmt n` | This assertion is true no more than n times | `assert x nmt 2;` |

`nft n` | This assertion is true no fewer than n times | `assert x nft 2;` |