October 2, 2026
SIGFPT Workshop Debrief and Formal Modeling Deep Dive with Shingai
Participants: _vgr, _shingai, anurajenp, ediblebadger, _ergod, heterotic, hitecsimp
The meeting served as a debrief on a recent workshop and symposium while diving deeper into Shingai's formal modeling research agenda. Shingai shared work on formalizing systems theory definitions and is using real protocols like Blygger as case studies. The group discussed the role of category theory in protocol formalization, noting it had been planned but not executed in previous years. Heterotic expressed interest but noted short-term availability constraints, while hitecsimp highlighted specific interest in symmetric monoidal categories and polynomial functors—areas particularly relevant to formal protocol theory but complicated by category theory's tendency toward multiple equivalent perspectives.
- Shingai is developing formal models for protocol systems, with a focus on formalizing definitions from systems theory literature using Lean, and is exploring real-world protocols like Blygger as case studies.
- The group identified category theory as an important but under-explored area for SIGFPT, noting that symmetric monoidal categories and polynomial functors are particularly relevant to protocol formalization.
- There is ongoing tension in category theory discussions about multiple valid entry points and descriptions, which requires careful navigation when applying CT to protocol analysis.
- The symposium Q&A was successfully captured and synthesized into Shingai's published work on protocols as systems.
Session Recording Summary · 40m 20s · Full notes ↗
Reading: The session centered on Shingai Thornton's talk/write-up for the Protocol Institute's "atomic protocol"/SIG-FPT challenge, in which he attempts to find a common formal core across three mathematical definitions of "system" from the systems-theory tradition: - George Klir (transcribed "Clear"/"clears") — a set-theoretic definition (things + relations) - Mario Bunge (transcribed "Boonghe"/"Boomhai"/"Mario Boomhai") - George Mobus (the "MOBUS"/"Mobis" formalism) The common formulation discussed was roughly `S = (T, R)` (a tuple of things/participants and relations), with a protocol framed as a set of participants plus rules constraining them.
After a round of feedback, Shingai described his academic context (PhD in Systems Science at Binghamton, advised by Cliff Joslyn) and his goal of building rigorous, diagrammatic modeling tools accessible to non-mathematicians. The bulk of the session was a probing Q&A: Patrick questioned whether a protocol is really a "system" or just the rules/relations, and whether "dependency" is a richer (directed) notion than a bare relation; Ergod pushed on where dynamics and emergence live in these static formalisms. The group closed with planning for next sessions, converging on category theory as the likely tool for the compositional ambitions.
- The synthesis approach. Shingai took several systems-theory definitions and tried to extract a common core. The one invariant he found across Klir, Bunge, and Mobus is some notion of dependency — things related such that they depend on each other. Ergod characterized this as a "synthesis relationship," looking for a common denominator.
- Protocol = rules, not the whole system. Patrick argued a protocol is better understood as the rules (closer to relations/edges) that mediate a system, not the system itself. Shingai agreed, noting Mobus is explicit that "a protocol is a set of rules... for how things cross boundaries," and that his own `S = (T, R)` framing was an artifact of how he and Claude attacked the challenge.
- Constructivism vs. realism. Shingai described Klir as an adamant constructivist — systems don't exist "out there"; humans impose systemness by choosing things and relations. Shingai leans realist: systems have independent existence, and he finds "things + relations" unnatural as a complete account.
- Relation vs. dependency (directedness). Patrick pressed: isn't a plain relation an undirected tuple/edge, whereas dependency implies a directed arrow ("a depends on b")? Why isn't Klir's minimal, undirected version the more fundamental one? Shingai clarified Klir makes no assertion about direction — arbitrary relations, no directed graphs, no baked-in dependency. Bunge and Mobus, by contrast, do assert flows and directed graphs in their core math.
- Where dynamics live. Ergod distinguished three "powers" of a model: descriptive, computational, and prescriptive (e.g., prescriptive = telling you things about protocol design). He argued `S = (T, R)` only gives a static snapshot. Shingai agreed dynamics are added later in Klir (via a "mechanism" component, history, and a time interval Δt), whereas he personally believes dynamics should be baked in — which is why he's biased toward the more complex Mobus/Bunge definitions.
- Dependency doesn't explain why. Ergod drew on his own experience building a code-base dependency graph (to compute "blast radius" of a change): a dependency graph shows how far a change can propagate but "doesn't tell you why anything changes." He wants models that let dynamics flow and let structure (e.g., a protocol, a technology) emerge, rather than models where the sought-for thing is smuggled in as a seed ("when they find it, it was already there").
Questions & Disagreements: - Is a protocol a system or just its rules? Patrick vs. the `S = (T, R)` framing; Shingai largely conceded Patrick's point. - Relation vs. dependency: Patrick asked whether dependency (directed) is strictly more structured than a bare relation, and if so why Klir's minimal version isn't the most fundamental. Shingai acknowledged this might be "getting at something fundamental" that would …
Participants: Patrick Nast, Robby Rao, Venkatesh Rao, Shingai Thornton, Giovanni Merlino, Ergod