# Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

arXiv: https://arxiv.org/abs/2608.00882 · HTML: https://mlsanity.com/paper/2608.00882/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 15 of its 41 references that are in the map.
- First posted on arXiv 1 Aug 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 15 of 15)

- [Nonmalleable Information Flow: Technical Report](https://mlsanity.com/paper/1708.08596/) (2017)
- [Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)](https://mlsanity.com/paper/2301.10037/) (2023)
- [AI-Assisted Completion of CertiGC Proofs: An Experience Report](https://mlsanity.com/paper/2606.21167/) (2026)
- [Calculational Design of Information Flow Monitors (extended version)](https://mlsanity.com/paper/1605.02778/) (2016)
- [Reconciling progress-insensitive noninterference and declassification](https://mlsanity.com/paper/2005.01977/) (2020)
- [Thirty-seven years of relational Hoare logic: remarks on its principles and history](https://mlsanity.com/paper/2007.06421/) (2020)
- [Towards a General-Purpose Dynamic Information Flow Policy](https://mlsanity.com/paper/2109.08096/) (2021)
- [Alignment complete relational Hoare logics for some and all](https://mlsanity.com/paper/2307.10045/) (2023)
- [Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version)](https://mlsanity.com/paper/2309.03442/) (2023)
- [Security Properties through the Lens of Modal Logic](https://mlsanity.com/paper/2309.09542/) (2023)
- [Automated Software Verification of Hyperliveness](https://mlsanity.com/paper/2403.03323/) (2024)
- [Nonmalleable Progress Leakage](https://mlsanity.com/paper/2505.12210/) (2025)
- [Forall-Exists Relational Verification by Filtering to Forall-Forall](https://mlsanity.com/paper/2509.04777/) (2025)
- [Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)](https://mlsanity.com/paper/2602.20082/) (2026)
- [Compositional security definitions for higher-order where declassification](https://mlsanity.com/paper/2604.18300/) (2026)

## Abstract (arXiv)

Many high-level security requirements are about the allowed flow of information in programs and are difficult to make precise because they involve selective downgrading. Notions from epistemic logic have emerged as a good approach to policy semantics but a robust general framework remains elusive. A paper appearing in CSF 2018, entitled ``Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies'', attempted to provide a unifying framework---but the formalization was sketchy and a correction was announced during the conference presentation. With aid from an agentic AI coding assistant, a corrected formalization has been machine checked in the Rocq proof assistant. The simplicity and generality of the framework may help compare different policy specification styles and enforce them by leveraging existing techniques.