Auditing Formal Verification of AI Model Weight Security Through Debate

The capabilities of an AI model reside in its weights, so whoever steals them can misuse the model. For this reason, RAND defines security levels for frontier AI providers, and its Security Level 3 framework lists 262 controls against organised cybercrime and insider threats. To show an auditor that a control is in place, a provider can verify its implementation formally, for example through model checking. However, this evidence is as strong as the specification behind it, and the auditor usually sees only part of the infrastructure. So this project studies two questions: which controls formal evidence can demonstrate, and how an auditor can accept that evidence through a debate, in which the provider submits its specification and proof and an auditor panel of language models challenges them. To ground both, I am building SL3-FrontierLab, an open-source laboratory that implements Security Level 3 controls with existing open-source software and records which control each design decision meets.

14 Nov 2026 — 15 Nov 2026