Model checking a live blockchain bridge with Specl
speclformal-verificationmodel-checkingblockchaindistributed-systems
Blog
Technical articles on distributed systems, concurrency, and software engineering.
18 Feb 2026
Specl progress: symbolic checking, 1.7x faster than TLC, more example specs, and a reference manual
speclformal-verificationmodel-checkingdistributed-systemsperformancesymbolic
We're symbolic: finding the EPaxos bug with Specl BFS and symbolic modes
speclformal-verificationmodel-checkingdistributed-systemsepaxosconsensus
Specl: a faster TLA+ for the rest of us
speclformal-verificationmodel-checkingdistributed-systems
fastc: zero-config atomic commits from git diffs
toolsllmgit
Gmail Organiser: automatic email classification with LLMs
toolsllm
1Password Organiser: LLM-powered vault cleanup
toolsllm
Lower bound on the number of rounds in crash stop synchronous consensus
concurrency
Why does Jepsen Work?
math
Tech Talk - Interchain Security: Blockchain Scalability and Security
blockchain
How AWS builds things: Amazon Builder's Library. TLDR.
sweng
Large-scale Incremental Processing Using Distributed Transactions and Notifications a.k.a. Percolator
concurrency
Chain Replication
concurrency
Primary Backup Replication
concurrency
Concise TLA+ tutorial with state enumerating and symbolic model checking
sweng
Lower bound (space) on FIFO mutual exclusion in shared memory
concurrency
Lower bound (time) for read-write register in message passing
concurrency
Get started with TLA+ tutorial video
concurrency
Tech Talk - Modelling the Agoric smart contract kernel using TLA+
concurrency
Lower bound (time) on approximate agreement in shared memory
concurrency