Open

The Secure Program Synthesis Fellowship

Apart Research

Apply to mentor

Apply to participate

Structure

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.

For background on the framing, see How to Solve Secure Program Synthesis, The Scalable Formal Oversight Research Program, and Lies, Damned Lies, and Proofs.

A joint initiative of Apart Research and Atlas Computing.

Key Dates

April 28th - May 9th 2026: Mentor Applications open
May 18th 2026: Mentors Announced and Participant Applications open
May 31st 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.”

For further reading, see Specifications Don't Exist, Spec-elicitation paper

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.

For further reading, see: lean-tcb (GitHub),On the Promises of 'High-Assurance' Cryptography

Spec-Driven Development & Evaluation

Explore workflows where specifications generate multiple candidate implementations, which are then evaluated against each other. Projects may involve building infrastructure to compare robustness, correctness, or performance across implementations derived from the same spec.

For further reading, see: Approximately Aligned Decoding, Zero-DoF Programming

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.

For further reading, see: Who Watches the Watchers?, Validating Proofs

Full list of mentor projects coming soon.

Details

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.

Resources

For a curated list of secure program synthesis work across the field, see awesome-secure-program-synthesis.

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 in it for the mentors?

A few things:

A team executing your research vision. You propose the project; an Apart project manager and mentees run it with you. You’re directing the research, not running the project solo.
A dedicated project manager. An Apart Research Project Manager (RPM) handles the operational side of running a research team, so that you can focus on the research direction.
A working trial of potential hires. Historically, organizations running programs like this have used them functionally as work trials. Over four months you’ll work closely with mentees who’ve already passed our bar, giving you a clear read on who might be a fit for your team.
Project resources for the team: compute, and API credits.
Possibly a stipend. By default mentor roles aren’t paid, but if compensation would enable your participation, indicate this in the application form.

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