Search results

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

Status: Open.

#174 In tlaplus/Examples;

· lemmy opened on Jun 23, 2025

Simplify contribution process

Status: Open.

#171 In tlaplus/Examples;

· ahelwer opened on May 21, 2025

Should new learning exercises be placed in this repo?

Status: Open.

#167 In tlaplus/Examples;

· hwayne opened on Feb 28, 2025

Add proof checking time to manifest details

Status: Open.

#123 In tlaplus/Examples;

· ahelwer opened on Mar 2, 2024

Can't come up with working model for cbc_max or spanning

Status: Open.

#114 In tlaplus/Examples;

· ahelwer opened on Jan 23, 2024

Bakery-Boulangerie specs don't satisfy <code>DeadlockFree</code> or <code>StarvationFree</code> liveness properties

Status: Open.

#109 In tlaplus/Examples;

· ahelwer opened on Jan 18, 2024

Add some Apalache models

enhancement

Status: Open.

#108 In tlaplus/Examples;

· ahelwer opened on Jan 18, 2024

GitPod &amp; Codespaces - make sure bitrot hasn't set in

Status: Open.

#106 In tlaplus/Examples;

· ahelwer opened on Jan 18, 2024

Specs failing proof validation

Status: Open.

#67 In tlaplus/Examples;

· ahelwer opened on Feb 17, 2023

More termination detection algorithms

enhancement

Status: Open.

#45 In tlaplus/Examples;

· lemmy opened on Dec 22, 2021

Basic math exercises

enhancement

Status: Open.

#23 In tlaplus/Examples;

· lemmy opened on Oct 20, 2020

Towards beginner friendly examples

enhancement

help wanted

Status: Open.

#15 In tlaplus/Examples;

· lemmy opened on Apr 16, 2020