Commits

Branch selector

 master

User selector

All users

All time

Commit history

Commits on May 25, 2026

• CI: filter on max proof time in manifests (#213)

  Show description for 47b0e2c
  ahelwer

  authored
  47b0e2c

  Copy full SHA for 47b0e2c

Commits on May 14, 2026

• CI: record proof runtime (#206)

  ahelwer

  authored
  32a32c7

  Copy full SHA for 32a32c7

• Close missing BY clauses in TypeOK_Step network cases

  Show description for 3a6b92c
  

  3 peoplecommitted
  3a6b92c

  Copy full SHA for 3a6b92c

Commits on May 13, 2026

• Remove outdated Folds and Functions modules from FiniteMonotonic

  Show description for 809c7a2
  lemmy

  committed
  809c7a2

  Copy full SHA for 809c7a2

• List the new `_proof.tla` files in per-spec manifest.json and README.md

  Show description for 3ea60a6
  

  lemmy

  and

  claude

  committed
  3ea60a6

  Copy full SHA for 3ea60a6

• Add TLAPS proof companions for example specifications

  Show description for 0ff8795
  

  lemmy

  and

  claude

  committed
  0ff8795

  Copy full SHA for 0ff8795

• Name unnamed ASSUMEs in three example specifications

  Show description for 92cf6dd
  

  lemmy

  and

  claude

  committed
  92cf6dd

  Copy full SHA for 92cf6dd

• tcp: add TLAPS safety proof for RFC 9293 state machine

  Show description for 82bc012
  

  lemmy

  and

  claude

  authored
  82bc012

  Copy full SHA for 82bc012

Commits on May 12, 2026

• BlockingQueue: bump submodule to v39

  Show description for 3feca98
  lemmy

  committed
  3feca98

  Copy full SHA for 3feca98

Commits on May 8, 2026

• ewd998: move RECURSIVE SimpleCycle from Utils.tla to EWD998_anim.tla

  Show description for 8f94d8a
  

  lemmy

  and

  claude

  committed
  8f94d8a

  Copy full SHA for 8f94d8a

Commits on May 4, 2026

• Fix overlay tree edge definition in comment of EWD687a.tla

  Show description for b864582
  lemmy

  authored
  b864582

  Copy full SHA for b864582

Commits on Apr 25, 2026

• Add Apalache wrappers and configurations for example specifications

  Show description for 15733ef
  

  2 peopleauthored and

  lemmy

  committed
  15733ef

  Copy full SHA for 15733ef

• CI: skip Apalache checks on Unicode specs

  Show description for 38f89e1
  lemmy

  committed
  38f89e1

  Copy full SHA for 38f89e1

• CI: Default Apalache --length=5 for all examples

  Show description for aca8dca
  lemmy

  committed
  aca8dca

  Copy full SHA for aca8dca

• CI: invoke Apalache via apalache-mc.bat (and cmd.exe) on Windows

  Show description for f1aaf96
  lemmy

  committed
  f1aaf96

  Copy full SHA for f1aaf96

Commits on Apr 22, 2026

• Fix variable name in markdown table check script.

  Show description for d9ce4db
  lemmy

  committed
  d9ce4db

  Copy full SHA for d9ce4db

Commits on Apr 20, 2026

• CI: check proofs using find | jq | xargs bash pipeline (#205)

  Show description for 08f63a1
  ahelwer

  authored
  08f63a1

  Copy full SHA for 08f63a1

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