Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Apr 7, 2026

• Add DieHard graph

  Show description for b05b8ff
  lemmy

  committed
  b05b8ff

  Copy full SHA for b05b8ff

• Strengthen Live property.

  Show description for 957d9cd
  lemmy

  committed
  957d9cd

  Copy full SHA for 957d9cd

• TLCMC: non-strict BFS, BFS level tracking, state constraints,

  Show description for 1725845
  lemmy

  committed
  1725845

  Copy full SHA for 1725845

Commits on Mar 26, 2026

• Change loop step from 'l' to '1' in pseudo code comment of Bakery.tla

  Show description for dc6470a
  

  josef-widder

  authored and

  lemmy

  committed
  dc6470a

  Copy full SHA for dc6470a

Commits on Mar 18, 2026

• Fall back to Apalache v0.52.2 if latest download fails

  Show description for ec17f2a
  lemmy

  committed
  ec17f2a

  Copy full SHA for ec17f2a

Commits on Mar 2, 2026

• Add Apalache wrapper for DieHardest

  Show description for 9ac1cdc
  lemmy

  committed
  9ac1cdc

  Copy full SHA for 9ac1cdc

• DieHardest: compare jug configurations via self-composition

  Show description for db122e3
  lemmy

  committed
  db122e3

  Copy full SHA for db122e3

Commits on Feb 13, 2026

• Update comment of DieHarder specification to reflect three constant parameters.

  Show description for aaf4954
  lemmy

  committed
  aaf4954

  Copy full SHA for aaf4954

Commits on Jan 19, 2026

• Add "dag-based consensus" (#198)

  Show description for 05c7256
  nano-o

  authored
  05c7256

  Copy full SHA for 05c7256

Commits on Jan 16, 2026

• fixed failing proof in byzpaxos/VoteProof (#197)

  Show description for 00eb5b4
  muenchnerkindl

  authored
  00eb5b4

  Copy full SHA for 00eb5b4

Commits on Jan 15, 2026

• Add community modules path argument to proof checking script

  Show description for dc25f34
  

  lemmy

  and

  Claude Sonnet 4.5

  committed
  dc25f34

  Copy full SHA for dc25f34

• Logically revert: "Replace Functions and FunctionTheorems with Fork variants"

  Show description for b1bbfd5
  lemmy

  committed
  b1bbfd5

  Copy full SHA for b1bbfd5

Commits on Jan 13, 2026

• Add SlidingPuzzles animation specification

  Show description for c7dc34e
  

  lemmy

  and

  Claude Sonnet 4.5

  committed
  c7dc34e

  Copy full SHA for c7dc34e

• Add optimal solution commentary for Klotski puzzle

  Show description for 30efe07
  lemmy

  committed
  30efe07

  Copy full SHA for 30efe07

• Add Tower of Hanoi animation (#194)

  Show description for f1d4d49
  

  lemmy

  and

  Claude Sonnet 4.5

  authored
  f1d4d49

  Copy full SHA for f1d4d49

Commits on Jan 10, 2026

• Refine EWD998 animation formatting and the modules documentation. (#193)

  Show description for 3673694
  lemmy

  authored
  3673694

  Copy full SHA for 3673694

Commits on Dec 15, 2025

• CI: check all proofs without time limit (#191)

  Show description for c2641e6
  ahelwer

  authored
  c2641e6

  Copy full SHA for c2641e6

• adapting proofs to modified FS_Induction theorem (#190)

  Show description for dca6876
  muenchnerkindl

  authored
  dca6876

  Copy full SHA for dca6876

Commits on Nov 10, 2025

• CI: remove community modules details from manifest

  Show description for 0e018bc
  ahelwer

  committed
  0e018bc

  Copy full SHA for 0e018bc

Commits on Sep 10, 2025

• Replace Functions and FunctionTheorems with Fork variants

  Show description for 9ece37b
  lemmy

  committed
  9ece37b

  Copy full SHA for 9ece37b

Commits on Aug 22, 2025

• Manifest: added proof runtimes

  Show description for a3ecae1
  ahelwer

  committed
  a3ecae1

  Copy full SHA for a3ecae1

Commits on Aug 20, 2025

• Manifest: removed model size field in favor of runtime

  Show description for 3c0c83b
  ahelwer

  committed
  3c0c83b

  Copy full SHA for 3c0c83b

Commits on Aug 9, 2025

• Manifest: remove path, title, and description fields

  Show description for cad798e
  ahelwer

  committed
  cad798e

  Copy full SHA for cad798e

Commits on Aug 8, 2025

• Added B-tree spec to CI validation

  Show description for b209722
  ahelwer

  committed
  b209722

  Copy full SHA for b209722

• Added a B-tree TLA⁺ specification

  Show description for 5e90e0e
  

  lorin

  authored and

  ahelwer

  committed
  5e90e0e

  Copy full SHA for 5e90e0e

• Added barrier and peterson's algorithm specs to CI

  Show description for 18c5810
  ahelwer

  committed
  18c5810

  Copy full SHA for 18c5810

Commits on Aug 7, 2025

• Removed model (.cfg) file features from manifests (#182)

  Show description for 4414f33
  ahelwer

  authored
  4414f33

  Copy full SHA for 4414f33

• Adding Barrier synchronization and Auxiliary Variable examples (#177)

  Show description for 11c7cd8
  JarodDif

  authored
  11c7cd8

  Copy full SHA for 11c7cd8

Commits on Aug 1, 2025

• CI: Use TLAUC --skip numsets instead of unicode_number_set_shim.py

  Show description for 0b69aea
  ahelwer

  committed
  0b69aea

  Copy full SHA for 0b69aea

• Load manifests from outside examples repo

  Show description for a61fab6
  ahelwer

  committed
  a61fab6

  Copy full SHA for a61fab6

• Documentation now reflects split manifest.json

  Show description for c19a200
  ahelwer

  committed
  c19a200

  Copy full SHA for c19a200

• Manifest generation and state space recording scripts now use split manifests

  Show description for 4021e86
  ahelwer

  committed
  4021e86

  Copy full SHA for 4021e86

• Changed all scripts and CI to use split manifest

  Show description for d5af150
  ahelwer

  committed
  d5af150

  Copy full SHA for d5af150

• JSON schema and validation script now check split manifest

  Show description for f4f8613
  ahelwer

  committed
  f4f8613

  Copy full SHA for f4f8613

• Generated split manifests

  Show description for 682f431
  ahelwer

  committed
  682f431

  Copy full SHA for 682f431