Explore Primo and find a contribution

Use this map to connect the solver’s parts with explanations and open questions. Each card links to what exists today and a possible investigation. Open leads are proposals, not implemented features or assigned tasks. Read a lead’s scope and evidence before choosing work.

For the supported input boundary, start with the capability map. For a first run, use the getting-started guide.

Follow a query

This follows the default rebuild route for formulas without quantifiers. The search repeatedly consults theory solvers; it is not a single forward pass. Quantified input has its own route, shown below. Retained sessions have additional lifetime and backtracking requirements.

Choose a kind of contribution

A useful first contribution can be a focused test, explanation, or measurement. A solver optimization needs a justified mechanism and fresh correctness and performance evidence before acceptance.

If you enjoy…	A concrete starting point	How to proceed
Explaining difficult ideas	Work through an example in a chapter and identify a missing derivation or ambiguous term.	Documentation workflow
Finding counterexamples	Exercise a boundary such as backtracking, resource limits, or reconstruction after elimination.	Fuzzing and reduction
Experimental work	Investigate one bottleneck or an unresolved provenance/checking task.	Reproducible experiments and open evidence work
Algorithms and proofs	Choose a lead, read its primary sources, and specify invariants and unsupported cases before implementation.	Research register and literature map
APIs and data structures	Audit ownership or prototype an external library consumer before proposing interface changes.	Library API lead and contribution requirements

The correctness requirements apply across these areas. In the maintainer’s workspace, solver batches, fuzzing, and benchmarks belong in SLURM; contributors may use a suitable machine. The experiment workflow explains preparation and recording results. A card is a starting point, not a claim that its investigation is small or ready for implementation.

Find the rest of the manual

• Use the solver: input, models, and sessions.

• Look up exact behavior: options, effective policies, and tactic inventory.

• Understand the design: architecture and primary literature.

• Find proposals and ongoing work: open leads, documentation work, and results storage.

• Assess claims and history: evaluation evidence, documentation review, and preservation map.