## Counting the invisible: 30% of an LLM workflow's spend wasn't visible to the substrate.
What we measured against a real rate-limited provider when the substrate's accounting got more honest.

**Lamina**  **Token Accounting**  **Petri Nets**  **Rate Limits**  **Verification Substrate**

## Statically Bounding Resource Accumulation in LLM Agent Workflows: The Cost Case
A decidable, polynomial-time static analyzer produces a sound upper bound on the cumulative cost — and any monotone resource — accumulated across every reachable marking of an LLM agent workflow. Proven, implemented in Lamina, and evaluated against a live model across 25 parameter combinations with no violation.

**Lamina**  **Petri Nets**  **Formal Verification**  **LLM Agents**  **Cost Bounds**  **Static Analysis**
