💻 Working as a Software Engineer at Nvidia on TLA+.
Pinned Loading
-
tlaplus/tlaplus
tlaplus/tlaplus PublicTLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
-
tlaplus/CommunityModules
tlaplus/CommunityModules PublicTLA+ snippets, operators, and modules contributed and curated by the TLA+ community
-
BlockingQueue
BlockingQueue PublicTutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
-
tlaplus-workshops/ewd998
tlaplus-workshops/ewd998 PublicDistributed termination detection on a ring, due to Shmuel Safra:
-
lets-prove-blocking-queue
lets-prove-blocking-queue PublicProving a blocking queue deadlock free in a dozen different ways
-
tlaplus/vscode-tlaplus
tlaplus/vscode-tlaplus PublicTLA+ language support for Visual Studio Code
877 contributions in the last year
Skip to contributions year listDay of Week | July Jul | August Aug | September Sep | October Oct | November Nov | December Dec | January Jan | February Feb | March Mar | April Apr | May May | June Jun | July Jul | ||||||||||||||||||||||||||||||||||||||||
Sunday Sun | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Monday Mon | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Tuesday Tue | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Wednesday Wed | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Thursday Thu | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Friday Fri | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Saturday Sat |
Activity overview
Contribution activity
July 2025
Created 2 commits in 1 repository
Created a pull request in tlaplus/tlaplus that received 48 comments
Raise warning when definition or declaration appears as Record field name.
Alert users when record field names clash with existing definitions or declarations in TLA+. The primary purpose is to help users understand that f…
Opened 1 other pull request in 1 repository
tlaplus/tlaplus
1
open
-
Using
-dump
option to produce state dumps in machine readable format.This contribution was made on Jul 24
Reviewed 5 pull requests in 2 repositories
tlaplus/tlaplus
4 pull requests
-
Make TLCCache work in a constant context
This contribution was made on Jul 24
-
Raise warning when definition or declaration appears as Record field name.
This contribution was made on Jul 23
-
SANY: centralize log output streams
This contribution was made on Jul 22
-
SANY: replace custom Stack class with Deque
This contribution was made on Jul 17
tlaplus/foundation
1 pull request
-
Wrote July dev update newsletter
This contribution was made on Jul 21
Created an issue in tlaplus-community/tlauc that received 6 comments
Converting a spec containing Nat
causes Unknown operator:
ℕ'.
tlauc shouldn't convert an ASCII symbol to its Unicode equivalent if that Unicode symbol is not explicitly defined. For instance, converting Nat
to ℕ
…