Dates:
June - September 2026
Gross World LoC (Line of Code) is skyrocketing due to AI. By default, we have no way of knowing if what we're vibecoding is doing what we think its doing. Secure program synthesis, on the other hand, is the intervention for throwing advanced software correctness techniques at all the code coming out of the AIs.
This fellowship offers part-time research opportunities on mentor-led projects at the intersection of formal methods, AI systems, and security. Participants work in small teams to tackle challenging, underspecified problems in specification, validation, and adversarial robustness.
A joint initiative of Apart Research and Atlas Computing.
Key Dates
April 28th - May 5th 2026: Mentor Applications open
May 10th 2026: Mentors Announced and Participant Applications open
May 26th 2026: Participant Applications Close
June 9th 2026: Participants Announced
June 15th 2026: Projects Begin
July/August 2026: Mid-Project Presentations & Milestone Submissions
August/Septemer 2026: Final submissions
September/October 2026: Demo day
Focus Areas
Specification Elicitation
Develop tools and workflows for extracting formal specifications from ambiguous, distributed, or implicit sources (e.g., documentation, legacy systems, human stakeholders). Projects may include structured editors, GUIs, or pipelines that translate informal requirements into formal representations (e.g., Lean), building on approaches like “SpecIDE.”
Specification Validation
Design methods to verify that extracted specifications are correct and complete. This includes techniques for testing, cross-checking, or formally validating whether a specification accurately captures intended system behavior.
Spec-Driven Development & Evaluation
Explore workflows where specifications generate multiple candidate implementations, which are then evaluated against each other. Projects may involve building “arenas” to compare robustness, correctness, or performance across implementations derived from the same spec.
Adversarial Robustness for FM & QA Tools
Investigate failure modes in formal methods pipelines, LLM-assisted tooling, and QA systems. Projects may focus on adversarial inputs, robustness guarantees, or identifying weaknesses in automated reasoning and verification systems.
Full list of mentor projects coming soon.
Why This Matters
As code generation becomes cheaper and more scalable, the bottleneck shifts from implementation to specification and validation. Many real-world systems lack clear or complete specifications, and errors at this level propagate across all downstream implementations. Improving how we elicit, formalize, and validate specs is critical to building secure and reliable AI systems.
Program Overview
Projects are proposed by mentors and explored by small teams of mentees. The program emphasizes rapid iteration, exploratory research, and generating useful intermediate artifacts—even when problems are underspecified or intractable in full.
📅 Duration
- 4 months
- June - September 2026
🏢 Research Teams
- Expert Mentor + Apart Research Project Manager + Mentees
⏱️ Time Commitment
- Commitment of 8-30 hours a week per person
📍 Locations
- Remote
📋 Format
- Two research stages
- Workshop paper (or equivalent) → Demo day/Conference paper
🤝 Support
- Research guidance
- Compute
- APIs
- Community
- Demo day/Conference Travel funding
- Prizes
Projects and Mentors
Projects are proposed and guided by field leaders in Formal Methods and AI Security.
Our vision is high quality and productive collaborations that produce publishable and impactful work in a short time frame.
Projects and Mentors will be announced here once the Mentor Application Call has concluded.
FAQ
What background do I need?
No specific background is needed, so don't hesitate to apply. Useful skillsets include:
Proof engineering (in verified software preferred, but math proofs in ITP is somewhat fine)
Redteaming/pentesting, fuzzing, reverse engineering
SMT and model checking
Critical and secure systems design
Agentdev, ML benchmarks/evals/environments
What's the expected time commitment for mentors?
The minimum expected hours for mentors is 3hs/w. That being said, the more hours you can put, the higher the chances of you getting accepted as a mentor!
Is this paid?
By default, no. However, if a stipend would enable your participation, please indicate this in the application form or emailing us at secure-program-synthesis-fellowship@apartresearch.com
Can I participate while working full-time?
Only if you can dedicate at least 8 hours per week.
What if I’m not accepted?
You’ll stay in the Apart network for future projects and opportunities.
Other Questions?
Please email: secure-program-synthesis-fellowship@apartresearch.com
This fellowship is accepting project applications from mentors until May 5th.
