I want to write about something I have never used. That feels worth stating up front, because most of what I publish is work I have done, and this is not that. It is a thing I love from a distance and would like to try properly one day.

The Infobiotics Workbench is an in-silico software suite for computational systems and synthetic biology. Its modelling framework is stochastic P systems, a probabilistic extension of P systems, and it puts modelling, simulation, verification and biocompilation behind a single domain-specific language, the Infobiotics Language. Models are written, simulated deterministically or stochastically, checked formally, and eventually compiled towards genetic constructs.

I am not a biologist. What pulled me in was the shape of the abstraction.

Computation defined by boundaries

A P system computes with membranes. You have nested compartments, rules that fire inside them, and controlled transport of objects across their walls. The interesting question is never only what a rule does — it is what is permitted to cross which boundary, under what conditions, and what the system as a whole is therefore guaranteed to do.

That is almost exactly the question I spend my working days on. ChainPay is a set of compartments too: a mandate is a boundary, a spending limit is a rule on transport, an approved recipient is an eligibility check at the wall. Token-2022 transfer hooks are the same idea in a different vocabulary. I did not expect membrane computing to describe my own problem back to me in cleaner language, but it does.

The part I actually envy

Infobiotics analyses its models with the PRISM and MC2 model checkers, so you can state a temporal or spatial property of a stochastic, multi-compartment system and have it checked rather than argued about.

In payments I reason about that class of property constantly. No agent widens its own authority. No mandate settles twice. Every settlement produces a receipt. I currently defend those with tests, code review and careful reading. Biologists modelling a genetic circuit reach for a model checker. The gap between those two habits is not a gap in the tooling — PRISM exists, and people do apply it to protocols — it is a gap in my own training, and I would like to close it.

What I would try first

Something deliberately small. Two compartments, a population of objects in one, a rule that moves them across the membrane only under a stated condition, and then a property to check: that the second compartment never exceeds some bound, however the stochastic schedule falls out. That is a toy. It is also the exact shape of a spending limit, and I would learn more from getting one such model to pass than from reading another paper about it.

I have not done this. I have read about it, and I keep the tab open. It sits in the same part of my head as zero-knowledge proofs did two years ago, before I wrote any Noir — an interest I have not yet earned the right to call experience.

Someday. Probably starting with a model that fails, several times, before it says anything true.