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.
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/$.”
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.
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.
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.
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.
3-4 months- June - September 2026
Expert Mentor + Apart Research Project Manager + Mentees
Commitment of 8-30 hours a week per person
Remote
Two research stages -Workshop paper (or equivalent) → Demo day/Conference paper
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, such as $Erik Maijer/$and $Shririam Krishnamurthi/$.
Our vision is high quality and productive collaborations that produce publishable and impactful work in a short time frame.
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 3-4 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
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.
This listing may be aggregated from a public source or submitted by a third party. If you represent this employer and would like to update or remove this listing, contact support@aisafetycareers.com.