From accd7ffe189593376940ee3d09c82b957acb70c4 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Wed, 16 Dec 2020 13:27:23 +0100 Subject: [PATCH] Update README.md (#234) --- rust-spec/lightclient/README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/rust-spec/lightclient/README.md b/rust-spec/lightclient/README.md index e673cab5b..cdecb8fa4 100644 --- a/rust-spec/lightclient/README.md +++ b/rust-spec/lightclient/README.md @@ -187,7 +187,9 @@ defines the protocol that is executed on a full node upon receiving attack [evid - equivocation - amnesia -As is discussed in the [last part](attacks/isolate-attackers_002_reviewed.md#Part-III---Completeness) of the English specification, computer-aided analysis of [Tendermint Consensus in TLA+][tendermint-accountability] shows that these three types capture all possible attacks. +We discussed in the [last part](attacks/isolate-attackers_002_reviewed.md#Part-III---Completeness) of the English specification +that the non-lunatic cases are defined by having the same validator set in the conflicting blocks. For these cases, +computer-aided analysis of [Tendermint Consensus in TLA+][tendermint-accountability] shows that equivocation and amnesia capture all non-lunatic attacks. The [TLA+ specification](attacks/Isolation_001_draft.tla)