Skip to content
Apart Research
Apart Research
Contact us
Sprint projectFeb 2, 2026Bangladesh

VeriTrain - Formal Verification for AI Governance Compliance

Tasfia Chowdhury · Team VeriTrain

Submitted to The Technical AI Governance Challenge. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: VeriTrain - Formal Verification for AI Governance Compliance

Open in a new tab (opens in new tab)
Presentation

Presentation: VeriTrain - Formal Verification for AI Governance Compliance

Open in a new tab (opens in new tab)
Code (opens in new tab)
Share

VeriTrain is a system that lets AI developers generate machine-verifiable proofs that their training and deployment processes followed safety and regulatory rules without revealing code, data, or model details.

It uses a theorem prover, Isabelle/HOL, to check that properties like compute limits, mandatory safety evaluations, and deployment approvals were enforced. An LLM helps create the proofs, but the guarantee comes entirely from the formal verifier.

VeriTrain focuses on process verification rather than model behavior. The proofs can be shared with regulators or international partners to show compliance, making it a practical tool for trustworthy AI governance and international cooperation.

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. The project correctly identifies compute verification as an important unsolved problem for AI governance, and provides a nice overview of some example applications. The proposed formal verification, however, is applied at the wrong layer. Proving "N FLOPs < threshold" is _not_ the hard problem. The hard problem is ensuring the FLOP measurement itself is trustworthy. Since the proposed instrumentation accepts arbitrary inputs, there can be no trust in the outputs either.

    My suggestion would be to aggressively cut scope and go deeper. Instead of trying to build a full pipeline end-to-end, it would be more valuable to deeply investigate one specific link in the verification chain. A focused analysis of the trust model would be more impactful than a code base built around a flawed assumption. I would also suggest to be more precise about what was implemented vs. planned and to make the writing much more focused. Zoom in on one crucial problem and go deep first before attempting to scaffold a full system.

    Read full reviewShow less

  2. Good topic — as the paper well articulates verification without disclosure is a barrier to all international governance agreements, AI included. The formal verification architecture is sound, and the trace format design is thoughtful, conscious to only log aggregate statistics without risk to proprietary information. The main gap is that the system verifies compliance given the trace data, but cannot verify that the trace data accurately represents the actual training run. The paper's security evaluation acknowledges this, as instrumentation bypass attacks have a 66.7% success rate. The proposed mitigation is TEE attestation, but this would require the hardware infrastructure the paper notes isn't yet deployed at scale, and the paper expresses some wariness to hardware approaches early on. This means the architecture would work well as one layer in a verification stack, but needs to be combined with trusted trace generation (via TEEs or similar) before the "cryptographically unforgeable" framing fully applies. This a valuable component of a formal verification system, but does need many other components to be functional.

    Read full reviewShow less

Cite this project

@misc{chowdhury2026veritrain,
  title = {{VeriTrain - Formal Verification for AI Governance Compliance}},
  author = {Tasfia Chowdhury},
  year = {2026},
  month = feb,
  note = {Submitted to The Technical AI Governance Challenge, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/veritrain-formal-verification-for-ai-governance-compliance-gvyv}},
  url = {https://apartresearch.com/sprints/projects/veritrain-formal-verification-for-ai-governance-compliance-gvyv}
}

More from The Technical AI Governance Challenge

All 47 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026