Rodrigo Otoni

Tendermint inductive invariant violation

4

## Description When evaluating some specs in the [tendermint light-client repository](https://github.com/tendermint/tendermint/tree/master/spec/light-client/accountability) I found that some invariants do not hold when checked with the current version of Apalache. [Previous results](https://github.com/tendermint/tendermint/blob/master/spec/light-client/accountability/results/001indinv-apalache-report.md) indicate...

Invalid interpretations produced by Spacer

4

Hi, While trying to validate the interpretations generated by Spacer for a number of [CHC-comp](https://github.com/chc-comp/chc-comp22-benchmarks) instances, I believe I found some examples in which invalid interpretations are generated. Below is...

The SNEAKY bug in the arrays encoding

1

## Description The arrays encoding currently returns an unsound result when checking the invariant of the [mis](https://github.com/informalsystems/apalache/blob/main/test/tla/mis.tla) specification present in the integration tests. This was discovered during work on #1461....