Modular system synthesis beyond bounded soundness: unbounded mechanically checked correctness, scalability, and flexible orchestration of synthesized implementations and implementation-agnostic specifications (the MOSS open problems)

The MOSS framework (Park, Johnson, D'Antoni, Reps, FMCAD 2023) makes program synthesis scale by exploiting modularity: a layered system is synthesized one module at a time, alternating two synthesis primitives — synthesizing a module's implementation from an implementation-agnostic algebraic specification of the modules below it, and synthesizing such specifications from concrete implementations — so that each subproblem stays small and similar in character. The proof-of-concept MOSSKIT, built on JLibSketch and SPYRO over the SKETCH synthesizer, is only sound up to bounded loop/recursion unrollings and bounded input sizes, needs manually engineered grammars and manual tool-gluing, and requires the module-dependency graph to be a DAG processed strictly bottom-up. The paper leaves open how to turn this into a practical methodology: in particular, how to obtain unbounded, mechanically checked correctness of both synthesized implementations and synthesized implementation-agnostic specifications; how to automate grammar construction and scale specification synthesis to larger, richer libraries; how to avoid solver blow-ups via alternative backends; and how to relax the strict bottom-up synthesis order enforced when specifications are synthesized. The core remains open: the latest specification-synthesis tool in the lineage (LOUD, OOPSLA 2025) is still bounded-sound and explicitly reports that no verifier exists even for under-approximate (implicant) specifications, while adjacent SemGuS verification work provides solver-agnostic verification infrastructure but does not address the algebraic-specification modular setting.

Background

Program synthesis aims to construct a program automatically from a specification. In sketch-based synthesis (the SKETCH approach; Solar-Lezama 2013), the user writes a partial program with holes and the synthesizer fills them so the result meets a given specification, using counterexample-guided inductive synthesis (CEGIS): guess hole values, test against the specification, and use failing tests (counterexamples) to constrain the next guess. A fundamental limitation of SKETCH-style tools is bounded soundness: correctness is checked only for a bounded number of loop/recursion unrollings and bounded input sizes, so the synthesized program is guaranteed correct only within those bounds, not for all inputs.

An algebraic specification describes a module (e.g., a Stack) by equalities between sequences of operations, such as $pop(push(st,k))=st$, which hold for every implementation of the module's interface. JLibSketch (Mariano et al., OOPSLA 2019) extended sketching so that a client can be synthesized against such algebraic library specifications instead of concrete library code, representing the equalities as rewrite rules over algebraic data types (inductively defined data types such as lists or trees). SPYRO (Park, D'Antoni, Reps, OOPSLA 2023) attacks the inverse problem — specification synthesis: given a concrete implementation and a user-supplied grammar of candidate properties (a finite regular-tree grammar defining the domain-specific language $L$ of allowed formulas), it synthesizes a best $L$-conjunction: a set of properties each of which the implementation satisfies and none of which can be strengthened within $L$.

MOSS (Modular System Synthesis; Park, Johnson, D'Antoni, Reps, FMCAD 2023) composes these ideas into a methodology for synthesizing an entire layered system bottom-up. For each module interface $MI_i$, MOSS alternates (i) implementation synthesis: fill a sketch for module $i$ against an implementation-specific specification $\varphi_{imp}^{MI_i}$ (the concrete behavioral requirements this particular module's implementation must meet) while assuming only the implementation-agnostic specification $\varphi_{sem}^{MI_{i-1}}$ (algebraic equalities over the lower module's interface) of the layer below, and (ii) specification synthesis: derive $\varphi_{sem}^{MI_i}$ from the just-synthesized implementation, so that higher layers never need lower layers' code. Experiments with the MOSSKIT prototype showed the payoff: synthesizing Queue from the algebraic specification of Stack took 188 seconds versus 799 seconds from concrete implementations, and a TicketVendor module took 7 seconds where JLibSketch crashed on the monolithic problem; the workflow also exposed real bugs in published JLibSketch benchmarks (a HashMap mock mishandling hash collisions and an incorrect manually written ArrayList specification).

MOSSKIT, however, inherits severe limitations, which the paper itself enumerates. Soundness is bounded, inherited from SKETCH; the authors state as a future direction the integration with full verifiers such as Dafny (an automatic program verifier in which correctness proofs are checked mechanically for all inputs, not up to a bound), as SPYRO already did in a limited external experiment (Dafny verified 23/35 synthesized specification conjunctions fully automatically and 33/35 with manually supplied invariants or axioms). Specification synthesis with SPYRO requires finite grammars, and in practice the authors had to call it many times with hand-crafted smaller grammars and to hand-emulate JLibSketch's term-rewriting inside SPYRO. Unrolling nested loops blows up the number of synthesis holes. The framework requires the module-dependency graph to be a directed acyclic graph (DAG) and, when specifications are synthesized rather than hand-written, forces a strict bottom-up order. When the candidate property space $\Phi_i$ is infinite, no principled way is given to select a useful finite fragment, and the case studies showed a synthesized specification can be too weak for later clients (the ArrayList specification had to be strengthened by hand after SKETCH-generated violations revealed missing properties). The conclusion asks whether other synthesis approaches — enumeration, CEGIS variants, or equality-saturation frameworks such as egg (a technique that repeatedly applies rewrite rules to a term to discover equivalent forms) — can realize the two MOSS primitives.

Post-2023 work by the same group sharpens rather than closes the gap. LOUD (Park, Peng, D'Antoni, OOPSLA 2025) extends SPYRO to nondeterministic programs and to synthesizing both strongest over-approximating and weakest under-approximating (implicant) specifications, but its tool aspire is still built on SKETCH and its conclusion states that synthesized formulas are only sound up to a bound and that no existing verifier can reason about under-approximate specifications. The SemGuS line (SemGuS, for Semantics-Guided Synthesis, a general problem format for synthesis tasks stated over a formal program semantics; the SemGuS Toolkit, CAV 2024, is a solver-agnostic framework with parser, verifier, and enumerative solvers) and the reduction of SemGuS solution verification to validity in the $\mu$CLP calculus (a fixed-point logic combining least and greatest fixed points, generalizing constrained Horn clauses; Murphy, Johnson, Reps, D'Antoni, PLDI 2025) provide general infrastructure for verifying synthesized programs, but do not treat MOSS's setting of synthesizing against and synthesizing implementation-agnostic algebraic specifications of lower modules.

Problem Statement

Extend modular system synthesis (MOSS) so that synthesizing an entire layered system from module interfaces becomes a sound and practical methodology. The common scientific objective is to remove the gap between the MOSSKIT proof-of-concept and real modular synthesis tools. Within that objective, the MOSS paper poses two explicit research directions — unbounded, mechanically checked correctness of what MOSS synthesizes (facet 1 below; the paper's §V-E names integration with verifiers such as Dafny for full verification as future work), and whether other synthesis approaches can realize the two MOSS primitives (facet 3 below; asked in the paper's conclusion) — while facets 2, 4, and 5 elaborate limitations the paper records for MOSSKIT: hand-crafted finite grammars and the scalability of specification synthesis, the strict bottom-up order enforced when specifications are synthesized, and the absence of a principled way to select or strengthen specifications. The facets below articulate this common objective: they are independent directions rather than jointly mandatory parts, so addressing any one of them suffices, and a full answer to facet 1 (the core) alone resolves the central open problem.

1. Unbounded, mechanically checked correctness (the core): obtain full verification — for all inputs and unbounded recursion and loops, e.g., via integration with verifiers such as Dafny or other theorem provers, or via reduction to validity in a fixed-point logic such as $\mu$CLP or constrained Horn clauses (CHCs), the standard target logic for program-verification conditions — of (a) each synthesized module implementation against its implementation-specific specification $\varphi_{imp}^{MI_i}$ (under the assumed implementation-agnostic specifications of the lower modules), and (b) the soundness of each synthesized implementation-agnostic specification $\varphi_{sem}^{MI_i}$ with respect to the implementation it was synthesized from, i.e., mechanically checking that the implementation satisfies every property in the specification (the Soundness clause of the MOSS paper's Definition 5 of specification synthesis; its Precision clause — that no property can be strengthened within the candidate grammar — is a property of the synthesis procedure rather than part of the verification obligation), replacing today's bounded loop/recursion unrolling and bounded input sizes.

2. Scalability of specification synthesis and grammar design: automate the construction of the grammars of candidate properties (today finite, hand-crafted, and split into many small calls) and scale specification synthesis to larger and richer libraries than MOSSKIT's case studies, including string operations and more complex APIs.

3. Alternative backends and solver encodings: realize the two MOSS synthesis primitives (implementation synthesis from implementation-agnostic specifications, and specification synthesis) with approaches that avoid the current bottlenecks — hole explosion from nested-loop unrolling in large sketches, and the expressiveness limits of reasoning about algebraic datatypes via rewrite rules (including rewrite-cycle avoidance) — for example enumeration-based solvers, CEGIS variants, or equality-saturation frameworks such as egg, or richer solver encodings.

4. Flexible synthesis ordering within the layered setting: support synthesizing modules in orders other than strictly bottom-up — e.g., via partial specifications or incremental strengthening — so that implementations of lower modules need not be synthesized first. The MOSS paper's layered setting keeps the module-dependency structure acyclic (its Definition 1 assumes a strict linear order of layers, with dependencies forming a directed acyclic graph in general), and it notes that any synthesis order is already possible when the user is willing to write the implementation-agnostic specifications manually; the limitation it records is that synthesizing the specifications forces the strict bottom-up order.

5. Expressiveness of implementation-agnostic specifications: when the candidate property space $\Phi_i$ is infinite, give a principled way to select a practical finite fragment that is sufficiently expressive for clients yet searchable (the MOSS paper notes that one can build tools that find a 'good' set of properties and stop without trying to find an exhaustive set); and give principled criteria for when a synthesized specification $\varphi_{sem}^{MI_i}$ is strong enough for the clients that consume it — the modules of the layered design that synthesize against $\varphi_{sem}^{MI_i}$, a domain fixed by the design rather than chosen by the answer — or how to minimally strengthen it when it is not. In the MOSS paper's case study, the synthesized ArrayList specification proved too weak to prove the algebraic specifications needed by its HashMap clients, a weakness discovered only through violations generated during client synthesis and repaired by manual strengthening.

An answer must preserve what MOSS established: per-module synthesis subproblems of similar character, clients synthesized without seeing lower modules' implementations, and the ability to synthesize both implementations and the implementation-agnostic specifications consumed by higher layers.

References

1. Kanghee Park, Keith J. C. Johnson, Loris D'Antoni, and Thomas Reps. Modular System Synthesis. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD 2023). DOI: 10.34727/2023/isbn.978-3-85448-060-0_34; arXiv:2308.06956. https://arxiv.org/abs/2308.06956
2. Kanghee Park, Loris D'Antoni, and Thomas Reps. Synthesizing Specifications. Proceedings of the ACM on Programming Languages 7(OOPSLA2), 2023. DOI: 10.1145/3622861; arXiv:2301.11117. https://doi.org/10.1145/3622861
3. Kanghee Park, Xuanyu Peng, and Loris D'Antoni. LOUD: Synthesizing Strongest and Weakest Specifications. Proceedings of the ACM on Programming Languages 9(OOPSLA1), 2025. DOI: 10.1145/3720470; arXiv:2408.12539. https://doi.org/10.1145/3720470
4. Charlie Murphy, Keith J. C. Johnson, Thomas Reps, and Loris D'Antoni. Verifying Solutions to Semantics-Guided Synthesis Problems. Proceedings of the ACM on Programming Languages 9(PLDI), 2025. DOI: 10.1145/3729320; arXiv:2408.15475. https://doi.org/10.1145/3729320
5. Keith J. C. Johnson, Andrew Reynolds, Thomas Reps, and Loris D'Antoni. The SemGuS Toolkit. In Computer Aided Verification (CAV 2024), Lecture Notes in Computer Science, vol. 14683, pp. 27-40. DOI: 10.1007/978-3-031-65633-0_2; arXiv:2406.01792. https://doi.org/10.1007/978-3-031-65633-0_2
6. Keith J. C. Johnson, Rahul Krishnan, Thomas Reps, and Loris D'Antoni. Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics. Proceedings of the ACM on Programming Languages 8(OOPSLA2), 2024. DOI: 10.1145/3689744; arXiv:2408.15822. https://doi.org/10.1145/3689744
7. Benjamin Mariano, Josh Reese, Siyuan Xu, ThanhVu Nguyen, Xiaokang Qiu, Jeffrey S. Foster, and Armando Solar-Lezama. Program synthesis with algebraic library specifications. Proceedings of the ACM on Programming Languages 3(OOPSLA), 2019. DOI: 10.1145/3360558. https://doi.org/10.1145/3360558
8. Armando Solar-Lezama. Program sketching. International Journal on Software Tools for Technology Transfer 15(5), 2013. DOI: 10.1007/s10009-012-0249-7. https://doi.org/10.1007/s10009-012-0249-7
9. Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. egg: Fast and extensible equality saturation. Proceedings of the ACM on Programming Languages 5(POPL), 2021. DOI: 10.1145/3434304. https://doi.org/10.1145/3434304