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

Specmut: Semantic Mutation Testing for Formal Specification Tightness

Tyler Rector · Team Specmut

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

Read the report

Report: Specmut: Semantic Mutation Testing for Formal Specification Tightness

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

This project develops Specmut, a mutation-based validation tool for formal specifications. The core problem is that formal verification can prove code satisfies a specification, but it cannot prove the specification is strong enough to capture the intended behavior. Specmut generates nearby specification mutants and measures how often those mutants are semantically distinguished, producing a tightness score called τ. In the LLM experiment, Qwen generated baseline Lean-style theorem specifications and then repaired them using Specmut feedback. The repaired specifications improved tightness on all three non-ceiling tasks: list reverse increased from median τ = 0.647 to 0.960, set insert from 0.571 to 0.923, and sorting from 0.136 to 0.960. Across 37 analyzable paired comparisons, the median improvement was Δτ = 0.3516, with Wilcoxon p = 5.21 × 10⁻⁶. The result shows that semantic mutation feedback can guide LLM-generated specifications toward stronger, more behavior-constraining formal statements.

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 paper presents a plausible way to evaluate specifications, by confirming that their meanings fluctuate with small edits. I get how a spec with extra redundant clauses isn't well-posed; such a spec should be shortened. However, I don't understand how adding constraints or modifying existing constraints can be a useful style of mutation, since these changes can have such large effects orthogonal to the spirit of an original specification problem. Also, it doesn't seem straightforward how to break significant specifications into discrete "constraints," just combined with conjunction.

    The LLM experiment doesn't make a lot of sense to me. Fixing the repair targets sounds like an excessive amount of help to the LLM. There also seem to be surprisingly few benchmark specifications, of surprisingly low sophistication each. Presumably they all use lists because a customized model-finder was built, where the numeric parameter simply determines the (maximum) number of list elements. Generalizing to the wide world of mathematical structures might not be easy.

    Read full reviewShow less

  2. Spec accuracy is crucial in secure program synthesis, and mutation analysis is a great candidate for testing it. The sprint led to a tool in this direction. Some next steps I'd look at: (a) are there different shaped mutations that are profitable? (b) how to push the experiment further -- can you test whether "tau" predicts spec accuracy? (c) survey what other people are doing or what transfers from related domains

Cite this project

@misc{rector2026specmut,
  title = {{Specmut: Semantic Mutation Testing for Formal Specification Tightness}},
  author = {Tyler Rector},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/specmut-semantic-mutation-testing-for-formal-specification-tightness-hoge}},
  url = {https://apartresearch.com/sprints/projects/specmut-semantic-mutation-testing-for-formal-specification-tightness-hoge}
}

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