CwicSpec
Aditya Thalang · Team CwicSpec
Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.
We built a prototype that conjectures candidate specifications for C functions by generating inputs, observing outputs with KLEE, and searching for equivalences between expressions. Inspired by QuickSpec, the project explores whether theory exploration can be applied to C programs. Our implementation is limited by insufficient search-space pruning.
Reviews
Thank you for this work!
So much software running today is still based on C –in a Mythos world is has become increasingly important that SWE task e.g. to fix up zero-day problems can be addressed swiftly and thoroughly. I'd recommend adding your project's relevance to wider AI safety to strengthen your framing.
The methods and findings section are very compact: I'd recommend expanding them with more key insights on e.g. the development process, insights the example functions you ran and results overview, etc.
Honest limitations section.
This project has a clear vision and correctly identifies a high-value target in this space. Applying theory exploration to C is an ambitious choice but unfortunately the scope seems too large to make reasonable progress over the course of a hackathon. A much narrower approach focused on MVP / quick wins would have helped with faster understanding and iteration on tractable parts of the problem-space.
The authors presented their claims and process candidly and concisely. A ~null result is useful content to produce and may guide future exploration of the domain. However, the results were extremely sparse, making it difficult to understand progress made in this hackathon. I would have liked to see motivating examples which might show promise, or even rough-and-ready analysis of scaling and traits of success/failure attempts.
Cite this project
@misc{thalang2026cwicspec,
title = {{CwicSpec}},
author = {Aditya Thalang},
year = {2026},
month = may,
note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
howpublished = {\url{https://apartresearch.com/sprints/projects/cwicspec-jzep}},
url = {https://apartresearch.com/sprints/projects/cwicspec-jzep}
}More from The Secure Program Synthesis Hackathon
- View project: Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents
Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents
Lida Safety
Specifications for real systems do not exist as one-shot artifacts: the user's intent emerges as they discover edge cases, rewrite drafts, and react to failing tests. We present an iterative pipeline that takes this …
- View project: AgentSpecGap
AgentSpecGap
solo-team
This prototype extracts rules from system prompts, tool descriptions, and runtime config. Rules are classified into one of interface validation, authorization check, workflow ordering validation, runtime validation, …
- View project: SpecGap Arena
SpecGap Arena
Obligation Cartographers
SpecGap Arena is a benchmark and framework that exposes how incomplete specifications let plausible but incorrect code pass public tests. It synthesizes missing semantic obligations (security boundaries, invariants, …