I’m starting a new series on things I will pre-commit to paying for if someone builds it, or points me to one that meets my stated needs.

For the first run of the series, I spent several minutes looking through our API trying to guarantee there was no way a user could ever see data from a different organization, except if the data has been shared publicly. There are a few common solutions for this, like single-tenant systems, one tenant per organization, where data is copied to a “public” system once shared publicly by the user, but this is one of several similar invariants I need to guarantee. You can’t use tenancy as a knowledge boundary for every possible invariant.

You also can’t write tests asserting that something isn’t possible, for the same reasons it’s always hard to prove a negative. Fuzzing is an option, but the strength of the proven invariants tends to depend upon the skill of the person writing the fuzz tests.

The Build

I’d love to have a symbolic execution tool where I could write out invariants and it would prove whether or not they’re true, ideally as part of our standard suite of tests. Add in some AI for natural language writing of invariants à la “thou shalt not allow users to access other users’ data unless its visibility is set to public” or “thou shalt not allow users to assign tasks to other users they are not set as an owner for” and I could throw together a set of invariants in an hour or two covering all our basic security needs.

Aircraft manufacturers and similarly risk-intolerant companies (with the possible exception of Boeing) tend to use verification tools like TLA+ to specify the behavior of their systems, and guarantee through mathematical proof that there are no combinations of conditions that can result in behavior outside of specified constraints. The rest of us don’t use these tools because they take too much effort to set up and use. Using language models to bridge that gap would be a great way of turning natural language into value, and I’d personally pay some small amount every month to be able to eliminate these risks.