Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 25, 2026Indianola, Iowa and San Jose, California

Grounding LLMs With Standards Documents

Chad Brewbaker, Suhaas Teja V. · Team Specification Team

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

Read the report

Report: Grounding LLMs With Standards Documents

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

We grounded LLMs with POSIX, WC3, etc standards documents and the LEAN4 source code and in the course of the weekend they are able to elicit several bugs in the Rust MIT Coreutils and Safari/Webkit codebases.

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. Would be useful to distinguish how trivial and non trivial the bugs are. Also, would be better to lead with saying how many proofs are complete instead of how many theorems are written.

  2. The paper presents an experience report of providing LLM agents with authoritative specification documents (RFC, IETF etc.) and asking agents to reimplement tools with formal specifications matching these documents. While this approach is not itself strictly new (most larger verification efforts have been partially driven using existing specs), the results of this experiment are a useful datapoint in shaping the space of securing software using llms.

    A couple of comments regarding the results:

    - the paper mentions several specification bugs, such as "BUG-SS-001" a bug in RFC 8941, regarding SameSite values. When digging into this, it seems RFC 8941 is Structured Field Values for HTTP (https://datatracker.ietf.org/doc/html/rfc8941), and the rfc does not contain any mention to samesite. Similar observation for the FTP one. It could be that I misunderstood or found the wrong spec, but this ambiguity does not help build trust in the results of the formalisation. This could have been helped with more rigorous vetting or links for the bugs.

    - the second comment would be that it seems like a common pain point was around the parser, and the challenge unifying ABNF grammars with lean's functions? I would suggest the authors look into parser combinators. In particular, Lean happens to have a rather robust and flexible parser combinator library built in (this is actually what is used to parse lean code itself), and the library allows writing parsers closer to ABNF form. As a separate aside, there is a rich literature on formally verified parsers which it might be helpful to adapt for this purpose.

    Read full reviewShow less

Cite this project

@misc{brewbaker2026grounding,
  title = {{Grounding LLMs With Standards Documents}},
  author = {Chad Brewbaker and Suhaas Teja V.},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/grounding-llms-with-standards-documents-ckul}},
  url = {https://apartresearch.com/sprints/projects/grounding-llms-with-standards-documents-ckul}
}

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