zkARc: Succinctly Verifiable Proofs for Neurosymbolic Natural Language Formalization and Verification

arXiv:2611.10031v1 Announce Type: new Abstract: Autonomous agents increasingly execute consequential actions on behalf of users, but ordinary middleware guardrails do not provide cryptographic proof that a policy was actually enforced. Their verdicts leave counterparties dependent on the operator unless they repeat the checks themselves, potentially exposing sensitive policies and inputs. We present zkARc, a modular proof-carrying framework that wraps each stage of Automated Reasoning checks (ARc) in an independent, succinctly verifiable zero-knowledge proof. ARc is a neurosymbolic system that translates natural language policies into formal logic and verifies AI-generated content against them using SMT solvers. zkARc certifies the planner's output, the policy's formalization, the action's