note · opened 2026-10-13 · updated 2026-10-17 · 0 comments
Deliver a standalone, API-accessible general-purpose proof assistant
Goal
Nikaia should provide a standalone, independently executable proof assistant that can be used by external tools and other programming languages through a stable public API.
«Nikaia provides a standalone, externally usable proof assistant that can systematically model and prove properties of data structures, functions, and loops, and independently check its proofs.»
This is a product-level goal, not a claim that all these capabilities are already implemented. The existing logic and solver architecture in “ADR-270” (https://github.com/Nikaia-Foundation/Nikaia/blob/main/docs/specification/adr/adr-270.md) is a starting point. The current limitations described in “ADR-269” (https://github.com/Nikaia-Foundation/Nikaia/blob/main/docs/specification/adr/adr-269.md) need to be addressed deliberately.
Subtasks
Standalone executable and stable public API
Deliver a standalone executable that accepts proof problems without requiring the Nikaia compiler or a Nikaia project.
Define and document a stable public API for submitting queries and retrieving results, proof certificates, and countermodels.
Provide a documented integration path for external tools and other programming languages, through a library API and/or a language-neutral protocol.
Specify supported input formats and compatibility/versioning guarantees for the API and proof formats.
General properties over data structures
Extend the logic beyond arithmetic-focused theories to express properties of structured data, including records, fields, tuples, algebraic data types, constructors, and pattern matching.
Define the semantics required for equality, aliasing, and mutable or shared data.
Provide a way to express assumptions, preconditions, postconditions, invariants, and goals independently of Nikaia-specific syntax.
Make supported theories explicit and extensible; report unsupported or undecidable cases as “unknown” rather than treating them as proved.
Function behaviour and effects
Model function behaviour through contracts, including preconditions, postconditions, and frame/effect specifications.
Support reasoning about function calls and composition of contracts, including propagation of relevant facts across call boundaries.
Define how side effects, mutable state, and state changes are represented and reasoned about.
Specify sound behaviour when a function implementation or contract is unavailable, incomplete, or cannot be proved.
General loop-invariant reasoning
Provide a way to state or infer loop invariants and prove initialization, preservation, and the loop-exit consequence.
Support invariants over structured data and program state, not only simple scalar arithmetic.
Define the intended balance between user-supplied invariants, invariant inference, and automated proof search.
Test loops involving nested control flow, mutation, and function calls.
Independently checkable proofs
Preserve distinct outcomes: “proved”, “refuted” (with a countermodel where supported), and “unknown” (with an explanation).
Produce proof certificates that can be checked independently of the solver that generated them.
Keep the trusted proof checker small and document the trusted computing base.
Ensure compiler optimizations and removal of runtime checks rely only on independently checked proofs, never on unchecked solver answers.
Logic coverage and solver roadmap
Define a roadmap for quantifiers, nonlinear arithmetic, and theories beyond the initial QF_LIA/QF_LRA focus.
Specify how additional theories and data types will be supported, including dedicated decision procedures or solver backends where needed.
Publish a capability matrix distinguishing implemented, planned, experimental, and unsupported features.
Add conformance tests and benchmarks against standard problem formats and established solvers.
Add soundness tests for certificates and regression tests for countermodels and “unknown” results.
Acceptance criteria
The proof assistant can be executed as a standalone program without invoking the Nikaia compiler.
An external program can submit a proof problem through a documented, versioned interface and consume a structured result.
The system can express and prove representative properties involving structured data, function contracts and effects, and loop invariants.
Unsupported cases are reported honestly rather than silently treated as proved.
Successful proofs include certificates accepted by an independent checker; refuted claims include usable countermodels where supported.
Documentation clearly describes the supported logic, limitations, soundness boundary, and roadmap for broader theories and automation.
Related design records
“ADR-270 — Logic and solver architecture” (https://github.com/Nikaia-Foundation/Nikaia/blob/main/docs/specification/adr/adr-270.md)
“ADR-269 — Current contract/proof limitations” (https://github.com/Nikaia-Foundation/Nikaia/blob/main/docs/specification/adr/adr-269.md)
“General-purpose” describes the intended direction, not a promise that every mathematical theory is decidable or every claim can be proved automatically. The system must remain sound, expose its limits, and allow users to supply specifications and invariants when automation is insufficient.
