FazBrowse GitHub Viewer | Trending | | Home

Tools: [Download Repo ZIP] [Original HTTPS Page]

Commits · tlaplus/Examples · GitHub

Commits

Commits on Aug 27, 2026

dag-consensus: state the assumptions of BlockDag and Sailfish

lemmy
and
claude
committed
ed3cc4c

Commits on Aug 24, 2026

btree: assume the state constants are distinct

lemmy
and
claude
committed
f2f1f98
Disruptor: assume exactly one writer in the SPMC spec

lemmy
and
claude
committed
c757b12

Commits on Aug 23, 2026

Disruptor: name the assumptions of RingBuffer.

lemmy
and
claude
committed
45c1cfd
Factor the TLC concerns out of btree into MCbtree

lemmy
and
claude
committed
d8ed081
btree: state the assumptions on MaxKey, MaxNode and MaxOccupancy

lemmy
and
claude
committed
9126be8
Factor the TLC concerns out of the Disruptor specs into MCDisruptor

lemmy
and
claude
committed
f3e248a
Disruptor: assume that Writers and Readers are disjoint

lemmy
and
claude
committed
2c59baa
Disruptor: name the assumptions of the SPMC and MPMC specs

lemmy
and
claude
committed
1cf3cad

Commits on Aug 19, 2026

CI: model-check a sample of the Unicode specs

lemmy
and
claude
committed
e296c31
CI: check manifest metadata once, before the matrix

lemmy
and
claude
committed
f5d877b
CI: stop checking Unicode specs on macOS

lemmy
and
claude
committed
8d69edb

Commits on Aug 18, 2026

CI: fix the guard that skips Apalache on Unicode specs

lemmy
and
claude
committed
584dc24
Separate the CMP abstraction from the FLASH protocol.

lemmy
and
claude
committed
a94afef
CI: use JDK 21 for Apalache and JDK 17 for TLC

lemmy
and
claude
committed
815dbe1

Commits on Aug 13, 2026

Create AI usage policy for TLA Examples (#225)

lemmy
and
claude
authored
4ac4050

Commits on Aug 9, 2026

CI: delete check_proofs.py script (#223)
ahelwer
authored
52c4c65

Commits on Aug 6, 2026

Revert "CI: use JDK 25 for Apalache and JDK 17 for TLC"
lemmy
committed
8cc6a04

Commits on Aug 5, 2026

Prove Safety relative to TypeOK instead of via a combined invariant

lemmy
and
claude
committed
c84456b
CI: use JDK 25 for Apalache and JDK 17 for TLC

lemmy
and
VoxlyAi-studios
committed
d2ee24d
ewd998: raise EWD998_proof budget from 4 to 6 minutes

authored and
lemmy
committed
e90bda3

Commits on Aug 4, 2026

CI: check proofs with --strict (#219)
vasilisnasopoulos
authored
352084b

Commits on Aug 3, 2026

EWD998: close the nine lemmas that were stated without proof (#218)
vasilisnasopoulos
authored
15d3c4d

Commits on Jul 29, 2026

State the checked properties as theorems

lemmy
and
claude
committed
12003f2
Check progress as liveness instead of as an enabledness invariant

lemmy
and
claude
committed
576932c
Check the Murphi Lemma_1 through Lemma_5 invariants

lemmy
and
claude
committed
9972397
Quotient the FLASH model by the scalarset symmetry

lemmy
and
claude
committed
71338ec
Type-check and symbolically check the spec with Apalache

lemmy
and
claude
committed
002206f
Check the two-node, two-datum configuration

lemmy
and
claude
committed
eee0c1f
Assign whole records where an action writes all of their fields

lemmy
and
claude
committed
840dfe0
Document the history variables

lemmy
and
claude
committed
920a226
Drop the write-only ghosts LastWrVld, LastWrPtr and LastInvAck

lemmy
and
claude
committed
92e4909
Name the three groups of variables that share a frame condition

lemmy
and
claude
committed
5234a7f
Split the multi-branch actions into disjoint guarded sub-actions

lemmy
and
claude
committed
9a809b2
Encode the directory's ShrSet and InvSet as sets of nodes

lemmy
and
claude
committed
fe957c7

Back | FazBrowse Home | New Git URL