PlusCal is a language for writing algorithms that translates into TLA+. It is an invaluable tool for reasoning about concurrency.

Writing good unit tests is hard. Ideally we use as little code as possible to cover as many use cases as possible. One tool to help with this challange is data driven tests.

What must be true of every state in all behaviors of a functioning traffic light?

What does a TLA+ specification look like?

EF core 7.0 introduces a new, more efficient way of upating one or more properties of several entities.