Hello, I’m Sunil Murthy Software Engineer with 8+ years of experience in enterprise software development, device management, and distributed systems. Currently working on client device management ...

TLC is an explicit-state model checker — it enumerates every reachable state. The state space grows exponentially with variables, constants, and interleavings. At some point, every TLA+ practitione...

Raw TLA+ is the underlying mathematical specification language. PlusCal compiles down to it. Understanding raw TLA+ gives you maximum precision and unlocks refinement, module composition, and compl...

PlusCal is an algorithmic language that transpiles into TLA+. You write imperative-looking code, the translator generates the TLA+ spec underneath, and the model checker (TLC) exhaustively explores...

A recurring pattern in cryptography: you have one master key and need to derive multiple purpose-specific keys from it, or you need to prove that two keys are mathematically related without reveali...

The intermediate article covered the object model, refs, the index, and how merge and rebase work at a high level. This goes further — into the details that matter when you’re debugging performance...

Most git tutorials teach you the commands — commit, branch, merge, rebase. This post goes a level deeper into how git actually stores and tracks your code. Understanding the internals turns git fro...

This is the keybinding reference I wish I had when I started using Emacs seriously. It covers the built-in defaults, the package bindings I actually use daily, and the muscle memory that makes Emac...

TLA+ has a small number of data structures — sets, functions, sequences, and records — but they compose into surprisingly expressive models. If you’ve read the introductory article and seen the bas...

The introductory article covered the fundamentals — state machines, PlusCal syntax, invariants, and basic model checking. This picks up where that left off. We’ll get into refinement mappings, spec...