POES (Proof-Oriented Event Sourcing) is an experimental Python library that brings formal verification techniques to event-sourced systems. It exploits the structural properties of event sourcing — pure apply functions, bounded state spaces, immutable events — to make verification tractable without a separate specification artifact. The library operates through four layers: property-based testing via Hypothesis, exhaustive BFS state exploration, temporal property checking using Tarjan's SCC algorithm, and persistence verification against real production data in KurrentDB. Guards, invariants, and post-conditions are expressed as Python lambdas embedded directly in domain code, eliminating the specification-implementation gap common in traditional formal methods like TLA+ or Coq. The library is designed to integrate with AI coding agents, enabling them to verify generated event-sourced aggregates automatically and receive minimal counterexamples when properties fail.
