Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 25, 2026Boston

SPS-VeriSpec

Zheng Wangyuan · Team SPS-VeriSpec

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

Read the report

Report: SPS-VeriSpec

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

We implemented a complete pipeline from Python program to Datalog properties to test cases.

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. I think it's a great idea to use Datalog-powered analysis for program understanding to create test cases, but the story of this tool doesn't hang together for me yet.

    First, in the setting of secure program synthesis, why is it helpful to analyze a program to generate tests for it? Don't such tests merely reinforce the bugs already present in the program, sometimes perversely requiring that buggy behavior be replicated in later versions? I don't understand how Figure 1 can be seen as providing empirical evidence that the tool is useful, since it is trivial to generate test cases that a given program passes, if only by rejection sampling.

    Second, the report is unclear on how Datalog analysis results are used to generate test cases. The report acknowledges that analysis so far mostly covers program structure rather than dynamic behavior, so where do useful tests even come from? Should we expect scalability of the underlying program analysis to much larger programs?

    Read full reviewShow less

  2. This projects has a mutation harness with named operators and it reports comparative kill rates, but most of the work is only in the repo and doesn't make it into the paper.

    SPS-VeriSpec's three-tier scheme (most restrictive properties become unit tests, mid-range become hypothesis property-based tests and open/risky ones go to a manual-review report) makes sense as an organizing idea, and the pipeline is implemented across three targets of increasing difficulty .

    The related-work section is candid that none of the components are new, and the literature is cited properly. A good design instinct is to set LLM-proposed rules and oracles as provenance-tainted review candidates, which is a right posture for secure synthesis.

    A promising next step is the one the author identifies, which is to close the loop so that when a generated test fails, the Datalog relation that produced it is surfaced for a human to accept, reject, or refine, with the decision persisted into the next analysis round, turning the current one-way pipeline into an iterative formal/informal loop. Curious what metrics for grounding come out of this.

    Read full reviewShow less

Cite this project

@misc{wangyuan2026spsverispec,
  title = {{SPS-VeriSpec}},
  author = {Zheng Wangyuan},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/spsverispec-sqhw}},
  url = {https://apartresearch.com/sprints/projects/spsverispec-sqhw}
}

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