I've been exploring Petri nets as a formalism for AI agent safety, specifically, proving properties like termination and human-gate enforcement exhaustively across every reachable state, rather than testing them on sample inputs. This post benchmarks the approach against n8n and ReAct on the same agent. Tomorrow I'm open-sourcing the engine as a declarative rules DSL.