Department of Computer, Control and Management Engineering

 

The deployment of large language models in high-stakes domains demands infrastructure for trusting AI-generated outputs whose reasoning is opaque and possibly beyond human comprehension. This talk introduces Proof-Carrying Output (PCO), a framework in which an AI system returns an answer accompanied by a machine-checkable proof of compliance with a published, decidable specification. The proofs rely on established proof assistants such as Rocq (Coq) for symbolic reasoning and on temporal logics (LTL, STL) for time-dependent properties. On top of proof checking, PCO adds a cryptographic accountability layer that binds the output, its proof, the validator version, and a trusted timestamp into a non-repudiable commitment on an append-only ledger before the output is acted upon, yielding binding, hiding, temporal ordering, and audit correctness. We demonstrate PCO through three case studies with working Rocq/STL implementations—tax computation, autonomous-vehicle compliance, and recommendation transparency—extending proof-carrying code from static programs to dynamic AI outputs, and we discuss specification-coupled small language models published by regulators as an enabling substrate for proof generation.

 

Additional recent results from my group will be described too.

 

Short bio:

Shlomi Dolev holds the Rita Altura Trust Chair in Computer Sciences at Ben-Gurion University of the Negev, where he was the founding chair of the Computer Science Department and served as Dean of the Faculty of Natural Sciences. He is an IEEE Fellow and an EAI Fellow, served as the chairman of the Israeli Inter-University Computation Center (IUCC), and the computer science committee of the Israeli ministry of education, currently head of the Negev Hi-Tech Faculty Startup Accelerator. Co-founder of Secret Double Octopus LTD and SecretSkyDB LTD. His research spans distributed computing, cryptography, self-stabilization, and post-quantum systems; he is the author of the book Self-Stabilization (MIT Press).