- Microsoft PROSE SDK – A platform for Program Synthesis by Example developed by MSR. PROSE provides APIs to define a domain-specific language (DSL) and then automatically learn programs in that DSL from user examples (PROSE Framework - Microsoft Research) (PROSE Framework - Microsoft Research). It powers features like Excel’s Flash Fill and Windows PowerShell’s
ConvertFrom-String. Developers can use PROSE (available via NuGet and on GitHub) to incorporate synthesis into applications (for text manipulation, data extraction, etc.). - Sketch – A open-source synthesizer (originally by Solar-Lezama) for the Sketch language. Sketch allows you to write partial programs with holes (
??) and asserts, and uses a SAT solver to fill the holes such that the asserts hold. It’s great for generating bit-level code or algorithmic tricks automatically. The code and a web demo were available from the MIT Computer-Aided Programming group. Although the original repository was on Bitbucket, there are maintained forks on GitHub. Sketch remains a go-to tool for research on constraint-based synthesis. - Rosette (solver-aided language) – Rosette is a Racket-based framework for building your own synthesizers and verifiers (Rosette: About). It provides language constructs to symbolically execute code and query an SMT solver for solutions. Essentially, you implement an interpreter for your DSL in Rosette, and Rosette takes care of generating constraints for synthesis or verification (Rosette: About). It’s been used to create everything from GPU shader synthesizers to web layout repair tools. If you want to experiment with synthesis without building a solver from scratch, Rosette is a powerful toolkit (with good documentation and examples).
- Synquid – A synthesis tool for functional programs from refinement types (by Polikarpova et al.). Given a polymorphic refinement type that describes what a function should do (pre/post conditions encoded in the type), Synquid performs backtracking search to construct a term that inhabits that type ([PDF] Program Synthesis from Polymorphic Refinement Types) (“Type-Driven Program Synthesis” by Nadia Polikarpova - YouTube). It’s particularly adept at creating recursive algorithms that satisfy complex properties (e.g., a sorting function that returns a sorted list). The Synquid solver and examples are open-source on GitHub. This is useful if you’re interested in type-driven synthesis research or need to generate tricky functional code with proofs.
- STOKE – A stochastic superoptimization toolkit from Stanford. It includes a compiler and optimizer that uses randomized program transformations to optimize x86 assembly code. You provide a target function and a cost metric (e.g., minimize runtime or code size), and STOKE will search for a functionally-equivalent variant that is optimal. Under the hood it uses a combination of Markov Chain Monte Carlo (MCMC) sampling and verification to ensure the output is correct (GitHub - praveenkulkarni1996/awesome-program-synthesis: An curated list of papers on program synthesis.). The source is available on GitHub. It’s a niche but interesting tool demonstrating synthesis for low-level performance.
- PCC (Programming by Circuit Synthesis) Tools: If you are interested in reactive or finite-state program synthesis (e.g., hardware circuits or controllers), tools like Strix and BoSy synthesize automata or circuits from temporal logic specifications. These stem from the reactive synthesis community (Church’s problem, etc.). Strix (2018) can solve LTL synthesis competently. While more specialized, they are worth noting as tools in the synthesis ecosystem (often used in formal methods and hardware design contexts).
- GitHub “Awesome Program Synthesis” List – A community-maintained curated list of papers, tools, and resources on program synthesis (GitHub - praveenkulkarni1996/awesome-program-synthesis: An curated list of papers on program synthesis.) (GitHub - praveenkulkarni1996/awesome-program-synthesis: An curated list of papers on program synthesis.). It includes sections for surveys (GitHub - praveenkulkarni1996/awesome-program-synthesis: An curated list of papers on program synthesis.), specific systems (Flash Fill, Sketch, etc.), and even links to research group pages. Browsing this list is a quick way to find key publications and implementations. (Do note that it may not be updated continuously, but it covers many classics.)
| Papers with Code – Program Synthesis – On paperswithcode.com, the Program Synthesis topic aggregates papers, code repositories, and leaderboards for related benchmarks ([Program Synthesis | Papers With Code](https://paperswithcode.com/task/program-synthesis/latest#:~:text=Program%20Synthesis%20,specification%20or%20set%20of%20requirements)). This is useful to track state-of-the-art results on popular synthesis benchmarks and to find open-source code for recent neural approaches. For example, you can find implementations for papers like DeepCoder, Neuro-Symbolic synthesis, etc., and see how they perform on tasks like the FlashFill benchmark or academic competitions. |