Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs

I love the emphasis on “agile” spec writing. When you say “specification,” people think waterfall, and they think of specifying every single little detail about a program.

It doesn’t have to be that way! The best specifications I’ve written are little models of a fraction of the whole system. As mentioned here, you can write multiple specifications, about different parts or different aspects of the system. Give it a shot.

Here’s an AI take too: we can generate a heck of a lot of code with more confidence if we do conformance checking. To wrangle AI, we should probably write more specifications, and test the generated implementation for conformance against the spec.