Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 24, 2026Singapore

Postern: a Lean-verified access gateway for agentic data lakehouse

Vincent Lau · Team Postern

Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: Postern: a Lean-verified access gateway for agentic data lakehouse

Open in a new tab (opens in new tab)
Code (opens in new tab)More on postern-web.pages.dev (opens in new tab)
Share

We address access control for data lakehouses queried by LLM agents. An agent's effective rights are context-driven — which principal it acts for, which task it is invoked under, which scope the caller granted — and the static *identity→role→permission* chain of RBAC cannot encode any of those axes. Per-engine row- and column-level security does not survive the ETL boundary; physical tenant segregation forfeits the cross-source joins that motivate the lakehouse. We propose plan-level rewriting against a **Biscuit-Datalog** policy [@biscuit] and present **Postern**, an artifact in three parts: (i) a rewriter $\mathrm{rewrite} : \mathit{Catalog} \to \mathit{Policy} \to \mathit{Principal} \to \mathit{Plan} \to \mathit{Option}\ \mathit{Plan}$ mechanised in Lean~4 [@lean4], inspired by Cedar's Lean authorization core [@cedar2024] but stated over plan-level outputs rather than per-request decisions, with nine `sorry`-free theorems (axioms bounded by `propext` and `Quot.sound`) plus a partly-mechanised Horn-fragment Datalog evaluator; (ii) a Rust capability-tracking layer inspired by Odersky et al. [@capabilities-agents-2026] — invariant brand lifetimes, sealed types, opaque-receipt sinks; and (iii) a reference-conformance harness binding Rust to the Lean reference on 18 cases. We evaluate on the Kaggle `transactions-fraud-datasets` schema and identify Biscuit attenuation, audience, expiry, key rotation, cross-relation joins, and differentially-private aggregation as the principal open problems.

Reviews

Judging this Sprint?

Review this project

Your public critique appears on this page without your name. Your private critique is not published; only the Apart team reads it. If you agree below, we share your review with grantmaking.ai (opens in new tab) and the Transformative AI Fund so strong projects can be funded.

Not shown on this page.

Shown on this page, without your name.

Only the Apart team reads this, and funders if you agree below.

Share my name publicly on grantmaking.ai *
Share my private critique with funders *

How much would this matter for AI safety if it worked? How innovative is it? For scores of 4-5: is this actually new to the field, or replicating recent work?

Scoring guide
  1. 1Negligible. No clear problem addressed, or no meaningful novelty.
  2. 2Limited. Addresses a real problem but with a generic or well-trodden approach. Incremental at best.
  3. 3Moderate. Clear problem with a reasonable approach; some novelty in framing or method beyond routine application of existing tools.
  4. 4Significant. Important problem with an original approach, or identifies a neglected problem area. A valuable contribution others could build on.
  5. 5Exceptional. Tackles a critical AI safety problem with a genuinely novel approach, or opens a new research direction. Clear theory of change. You'd be excited to share this with researchers in the area.

How sound are methodology, implementation, and findings?

Scoring guide
  1. 1Seriously flawed. Methodology broken, results uninterpretable, or implementation doesn't work.
  2. 2Weak. Approach has significant gaps: missing validation, flawed experimental design, or incomplete implementation.
  3. 3Competent. Technically solid given the short duration. Methodology makes sense, results are interpretable, limitations acknowledged, work builds toward clear conclusions.
  4. 4Strong. Thorough methodology with convincing validation. Results clearly support conclusions. Immediately useful for future work.
  5. 5Exceptional. Ambitious scope executed rigorously. Surprising findings, novel methods, or unusually robust validation.

How clearly are work, findings, and impact potential communicated?

Scoring guide
  1. 1Incomprehensible. Cannot determine what the project is actually claiming or doing.
  2. 2Hard to follow. Key information buried, missing, or diluted by excessive length. Significant effort to extract main points.
  3. 3Clear enough. Can understand the problem, approach, and results without undue effort. Core content clearly present: problem, method, findings, limitations.
  4. 4Well presented. Easy to follow, well-structured, appropriate level of detail. Target audience would get it quickly.
  5. 5Exceptionally clear. A pleasure to read. Complex ideas made accessible. Could serve as a model for how to present this type of work.

  1. Creating nine theorems in Lean and building a Rust conformance harness looks very promising. That said, some of gaps limit the practical impact: the lack of join support weakens the core use case, and the Rust capability model leaves enforcement open to common escape paths. Security guarantees also rely on large assumptions, particularly the unverified translation from the Lean model to DuckDB and known runtime side channels. Future work would benefit from verified joins and a semantic link between the formal model and execution layer.

  2. The incomplete proofs and small corpus contradict with the claims made with each other slightly. Data minimisation is a hard problem to solve and the engineering is good.

Cite this project

@misc{lau2026postern,
  title = {{Postern: a Lean-verified access gateway for agentic data lakehouse}},
  author = {Vincent Lau},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/postern-a-leanverified-access-gateway-for-agentic-data-lakehouse-hv2v}},
  url = {https://apartresearch.com/sprints/projects/postern-a-leanverified-access-gateway-for-agentic-data-lakehouse-hv2v}
}

More from The Secure Program Synthesis Hackathon

All 61 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026