Policy Is Not Proof: What Machine-Checked Declassification Changes for Security Teams

TL;DR for operators

When software is intentionally allowed to disclose some sensitive information, a release rule and proof of compliance should not be the same object. David A. Naumann’s Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI¹ repairs an earlier framework by giving permitted information release an explicit meaning, then separately defining whether an observer learned more than that policy allows.

The paper’s main formal result is stronger than a design proposal: within its well-specified reactive-program model, a program-oriented relational safety condition is machine-checked in Rocq to imply epistemic security for every observer level. That creates a useful assurance architecture for systems that intentionally downgrade information: define what disclosure means at the policy layer, verify a tractable implementation-facing condition, and prove that condition is sufficient for the confidentiality property that ultimately matters.

The agentic-AI component should be read differently. Claude Code contributed proof infrastructure and substantial proof work, but the author also reports incorrect formalizations, overly specific lemmas, inappropriate strengthening of assumptions, and missed repairs. This is an experience report from one expert-led development, not evidence that coding agents can autonomously own formal verification.

The policy must say what disclosure means before code can satisfy it

Consider a system allowed to reveal a sensitive fact only under a particular state or event condition. A security team needs to answer two separate questions.

First: which hidden possibilities is the system permitted to rule out for an observer?

Second: does the implementation rule out anything beyond those possibilities?

The earlier 2018 framework that this paper repairs blurred those layers. Its program annotations expressed assumptions about permitted release, but the semantics did not cleanly establish release policy as an independent object before using it in the security condition. The new paper makes that separation explicit.

The starting point is an observer’s knowledge. Instead of treating “knowledge” as a scalar score, the framework represents it as a set of complete input histories still compatible with what the observer has seen. As outputs arrive, that set may shrink. Security becomes a constraint on how much shrinking is allowed.

The paper then defines a release policy as the set of alternative input histories compatible with the relational assumptions encountered along an execution. Those alternatives are constructed through aligned actual and alternative program pre-runs. In plain language, the policy specifies which alternative hidden worlds must remain plausible after intentional disclosure.

This gives security teams a cleaner abstraction boundary: an annotation in source code can help express a policy, but the policy’s meaning is not identical to the fact that the code contains that annotation.

Security is measured by what an observer can eliminate

The paper uses a progress-insensitive definition because observing that a system continues to produce visible events can itself reveal information. It therefore separates ordinary observer knowledge from progress knowledge: what remains possible given both prior observations and the fact that another visible event can occur.

The step-level security condition is:

The direction of the containment is the key. After the next event, the observer must still consider possible every input history that was both compatible with permitted progress leakage and protected by the release policy.

Security is therefore not “the observer learns nothing.” Intentional disclosure is allowed. The constraint is that an observable event cannot eliminate more hidden possibilities than the explicit policy authorizes.

For operational governance, this changes what should be reviewed. A confidentiality specification should identify the permitted reduction in uncertainty independently of the implementation mechanism that produces the disclosure. Otherwise, an implementation-specific condition can quietly become its own definition of acceptable behavior.

Relational safety turns policy into something an implementation can justify

An epistemic condition is useful as a specification, but it is not necessarily the easiest property to establish directly over code. The paper therefore introduces a relational safety condition that compares an actual execution with alternative executions.

Aligned pairs of executions are classified into five cases:

The paper proves this classification exhaustive and mutually exclusive. More importantly, Section 5.2 establishes the central result: under the paper’s model, relational safety implies epistemic security.

This is the main evidence, not a robustness exercise or illustrative extension. The theorem supplies the bridge between an implementation-oriented condition and the higher-level confidentiality requirement.

For organizations building controlled information-release mechanisms, Cognaptus interprets this as a reusable assurance pattern:

policy meaning → implementation-facing evidence → machine-checked implication → confidentiality claim

The value is not that every enterprise system should adopt this particular semantics. It is that high-stakes controls benefit when the condition engineers can check is explicitly proved sufficient for the policy property management actually intends to enforce.

Rocq caught errors that coherent-looking mathematics had not removed

The paper is itself a correction to earlier work, and mechanization uncovered more than the already-known conceptual flaw. The Rocq development exposed additional problems involving divergence, knowledge definitions, and subsidiary lemmas.

That history makes machine checking part of the result’s practical significance. Multi-execution security arguments combine operational semantics, alternative traces, alignment conditions, knowledge sets, and declassification assumptions. A proof can remain persuasive on paper while one auxiliary definition or strengthened premise changes what the theorem actually establishes.

For a security engineering team, machine checking therefore serves a different purpose from ordinary documentation review. It tests whether the claimed implication follows from the formal definitions actually written down.

The boundary is equally important. The theorem applies to the paper’s deliberately simplified reactive language and well-specified-program assumptions. The work does not yet provide compositional proof rules for establishing relational safety in realistic systems, and the author identifies that as an open problem. The result is a verified theoretical bridge, not a turnkey production verification stack.

Claude Code accelerated proof work without earning specification authority

The title may invite a stronger AI claim than the evidence supports. Claude Code did not autonomously repair the theory and hand back a verified result.

The author describes roughly three weeks of AI-assisted Rocq work, around an hour per day, with the assistant able to access the LaTeX source, proof development, shell tooling, and a Rocq MCP server. It generated useful proof infrastructure and completed both routine and nontrivial proof tasks.

It also made errors at exactly the level where formal verification is most sensitive: incorrect definitions, lemmas tailored too narrowly to the immediate proof state, assumptions strengthened to make proofs easier, and failures to locate comparatively simple fixes.

Those observations are valuable as workflow evidence, but they are not a controlled evaluation. The interaction logs were not systematically analyzed, there was no productivity baseline, and the report comes from one experienced Rocq user.

The appropriate governance inference is narrower: agents can be given substantial proof-construction responsibility without being given final authority over what is being proved. Human experts still need to own the semantics, judge whether assumptions remain legitimate, reject abstractions that merely make proof search easier, and accept the final specification.

The deployable pattern is layered assurance, not autonomous proof generation

The paper offers a useful architecture for any organization dealing with deliberate release of protected information.

At the top is a policy meaning: what information may become knowable. Beneath it is a security property expressed in terms of the observer’s remaining possibilities. Beneath that is a program-facing condition that engineers may eventually be able to monitor or prove compositionally. Rocq then verifies the theorem connecting those layers.

That architecture is more transferable than the specific language formalized here. It prevents an implementation check from quietly redefining the policy it was supposed to justify.

The AI-assisted development points in the same direction. Automation can move deeper into proof construction, infrastructure generation, and local reasoning. Acceptance authority should remain attached to specification integrity and theorem meaning, because a formally completed proof can still certify the wrong claim if its definitions or assumptions drift.

Naumann’s repaired semantics therefore contributes two differently weighted results. The machine-checked safety-to-security theorem is high-assurance evidence within a bounded formal model. The Claude Code account is weaker but operationally instructive evidence about workflow design. Taken together, they support a security process in which both program checks and coding agents are treated as sources of evidence—not as substitutes for the policy layer or the expert who remains accountable for it.

Cognaptus: Automate the Present, Incubate the Future.