At the 24th Software Certification Consortium meeting, hosted at the Nuclear Regulatory Commission in Rockville, Joseph Kiniry gave a talk titled "The AI Wrote It, the Theorem Prover Signed It."
Walking a certification audience through the trust argument:
-
The objection that an LLM enlarges the trusted computing base is true only if AI is in the verification path. If AI is in the generation path, the proof kernel is still the trust anchor, same as it ever was.
-
"Signed" is literal: the theorem prover emits a machine-checkable certificate. Remove the AI from the pipeline and the certificate still replays.
-
Every HOARDE artifact carries a chain of custody: identity, provenance, model and seed, signed human review gate, machine-checkable certificate, and a dependency graph that propagates invalidation.
-
Policy enforcement is done through capability isolation, append-only audit logs, and non-repudiable review attestations. The resulting evidence maps directly onto CbyC, DO-178C, IEC 61508, and ISO 26262.
-
We discussed the hard questions: non-determinism (what's certified is verification, not generation), model drift (treat it like tool versioning), and spec fidelity (still the engineer's responsibility, but now with a lot of help).
Visual recap: The AI wrote it, the theorem prover signed it (PDF, 7 pages)
If you work on certified software, the conversation is just getting interesting and we'd love to talk. Get in touch.