Spec claims to check (safety-prop) `UnforgLtl` but config actually also checks (liveness-props) `CorrLtl` and `RelayLtl`

Open

#174 opened on Jun 23, 2025 5 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty: 2/5
Estimated time: 1-3 hours
Newbie friendliness: 35/100

Issue type: Bug
Clarity: Needs clarification
Activity status: Stale
Domain: testing

Research direction

Read the linked sections of specifications/bcastByz/bcastByz.tla and specifications/bcastByz/bcastByzNoBcast.cfg first, comparing the claimed properties with those configured for checking. Clarify which declaration is authoritative, then update the relevant specification or configuration so the documented and configured checks agree.

Written by the indexing model from the issue text.

Description

https://github.com/tlaplus/Examples/blob/c9938239d07bb16031c5a692b30f14c6bfb34471/specifications/bcastByz/bcastByz.tla#L173-L176

https://github.com/tlaplus/Examples/blob/c9938239d07bb16031c5a692b30f14c6bfb34471/specifications/bcastByz/bcastByz.tla#L210-L222

https://github.com/tlaplus/Examples/blob/c9938239d07bb16031c5a692b30f14c6bfb34471/specifications/bcastByz/bcastByzNoBcast.cfg#L6

Dominant language: TLA
Stars: 1.6k
Forks: 224
Avg merge: 7d 16h
Merged PRs (30d): 4

Contributor guide

Open the contributing guide

First steps

Read the whole issue, then the project's contributing guide.
Comment on the issue to say you are picking it up — it saves two people doing the same work.
Fork the repository and make your change on a branch.
Open a pull request that references the issue number.

Similar issues

[Puppeteer] Remove deprecated `getElementXY` helper and update usage Open

calcite-components needs triage refactor

Difficulty 2/5 1-3 hours Newbie friendliness 75/100

Esri/calcite-design-system#15203 · Opened Sep 21, 2026
🧹 Use PodSet wrappers in DRA tests Open

kind/cleanup

Difficulty 2/5 1-3 hours Newbie friendliness 88/100

kubernetes-sigs/kueue#15947 · Opened Sep 21, 2026
[quality-improver] Repository Quality: AzureFoundry Extension Missing from Self-Registration Acceptance Test Open

type/automation type/tech-debt

Difficulty 2/5 1-3 hours Newbie friendliness 78/100

microsoft/testfx#11431 · Opened Sep 21, 2026
Locale guard misses en_GB, so a removed key can survive in a shipped bundle Open

Difficulty 2/5 1-3 hours Newbie friendliness 91/100

0xMiden/wallet#1078 · Opened Sep 21, 2026
package: missing --cert file gives no guidance on how to create a certificate Open

Difficulty 2/5 1-3 hours Newbie friendliness 88/100

microsoft/winappCli#900 · Opened Sep 21, 2026

More Testing & QA issues