Programming Language designed for Program Synthesis with SMT-validation.
Start the server with python -m aeon --language-server-mode. Standard LSP
clients receive inferred types/refinements in hover and inlay hints, and errors
and warnings through textDocument/publishDiagnostics. No editor extension is
required for hover or diagnostics.
Hover over the body of either definition:
def inc (x:Int) : {v:Int | v > x} := x + 1;
def positive (x:Int) : {v:Int | v > 0} := x;
inc shows an inferred refined type and a valid verification obligation.
positive is rejected: hover shows the failing obligation and, when available,
a concrete counterexample such as x = 0. Diagnostics include machine-readable
data with kind: "refinement", status, obligation, counterexample, and
reason; clients that do not consume data still display the error message.
Statuses describe the actual verification pass:
valid: the solver proved the obligation (an unsatisfiable negation).invalid: the solver found a satisfiable negation; a counterexample is shown
when a concrete assignment can be rendered.unknown: the solver could not decide, for example because of a timeout.unsupported: translation failed; this is not a proof or a counterexample.Unknown and unsupported obligations are never accepted as proofs. A failed conjunction does not imply that every expression in it is wrong: failed aggregate obligations retain their aggregate status. Successfully verified conjunctions are split into source-located goals without additional solving. Proofs are collected during analysis, not reconstructed from a successful parse or from runtime samples. Cached solver results preserve their original status and reason. Syntax errors and document edits clear current proof evidence; last-good type information may remain available while editing.
def native_abs (x:Int) : {v:Int | v >= 0} := native "abs(x)";
The server warns that the Python implementation is trusted rather than
statically checked. Launch with --runtime-verification to enable runtime
checking of refined arguments/results when the program runs. The warning
reports whether that mode is enabled, but analysis does not execute the
program: it never claims that a runtime contract has passed. Imported native
definitions are not reported at unrelated positions in the current document.
Synthesis code actions and the aeon/infoView Synthesis tab expose every
registered synthesis algorithm, grouped by family. The list comes from
synthesizer_menu_ids() in the compiler’s synthesizer factory, including
CP-SAT (ortools), Contata, and each LLM backend/model. CLI aliases such as
tdsyn, cpsat, and llm remain accepted but do not create duplicate menu
entries. Optional backend dependencies are required only when running that
backend. The VS Code extension’s settings list can be refreshed from this
registry using its scripts/sync-synthesizers.py development script.
aeon/verification accepts {"textDocument": {"uri": "file:///path/example.ae"}}
and returns uri, obligations, runtimeVerification, and diagnostics.
Each obligation contains status, a source-facing obligation string,
reason, counterexample, a zero-based LSP range, cached, and scope.
Failed multi-goal conjunctions have scope: "aggregate" and a null range,
so their first (possibly valid) expression is not incorrectly blamed in hover.
Obligations without a real source location and trivial true goals are omitted.
runtimeVerification contains enabled and executed (always false during
analysis). Diagnostics contain message and their structured data.
The existing aeon/infoView request additionally accepts a zero-based
position. Its existing target, locals, globals, errors and synthesis options
remain unchanged; additive proofObligations and runtimeVerification fields
provide the same current-document verification evidence.
These requests are optional client extensions; the standard hover and diagnostic paths expose the essential information independently.