A DbC Inspired Neurosymbolic Layer for Trustworthy Agent Design
Claudiu Leoveanu-Condrei
TL;DR
The paper presents a Design by Contract (DbC) inspired contract layer for trustworthy agent design that mediates every LLM call with pre- and post-conditions defined over well-typed data. By modeling agents as $\mathcal{A} = { \mathcal{M}, \Pi, \Theta, \mathcal{T}, \mathcal{C} }$ and treating contract satisfaction as a probabilistic event, the approach provides verifiable, probabilistic guarantees and a notion of functional equivalence across agents satisfying the same contracts. The implementation leverages the SymbolicAI framework and Pydantic data models to encode types, a contract decorator to enforce validation, iterative remediation guided by semantic error messages, and a safe fallback to maintain operation even on contract failure; the success probability is computed as $P_{\text{succ}}=\tfrac{1}{N}\sum_{t=1}^{N} \mathbf{1}[\text{all contract predicates pass}]$. Limitations include stochastic LLM behavior and lack of formal guarantees, with future work outlining Lean4 formalization and grammar-constrained decoding strategies. Overall, this work offers a principled, declarative path to comparable, trustworthy agent designs that balance guarantees with LLM flexibility.
Abstract
Generative models, particularly Large Language Models (LLMs), produce fluent outputs yet lack verifiable guarantees. We adapt Design by Contract (DbC) and type-theoretic principles to introduce a contract layer that mediates every LLM call. Contracts stipulate semantic and type requirements on inputs and outputs, coupled with probabilistic remediation to steer generation toward compliance. The layer exposes the dual view of LLMs as semantic parsers and probabilistic black-box components. Contract satisfaction is probabilistic and semantic validation is operationally defined through programmer-specified conditions on well-typed data structures. More broadly, this work postulates that any two agents satisfying the same contracts are \emph{functionally equivalent} with respect to those contracts.