Cegis¶

cegis - mvp.cegis.

Cluster: Formal Verification | Type: component | MCP Tools: 39

Overview¶

Counter-Example Guided Inductive Synthesis (CEGIS) engine that synthesises programs from sketches with holes, verifying candidates against oracle test cases with progressive LLM agency reduction.

Scope and production limits

cegis is intended for narrow, well-scoped Python synthesis problems: simple functional specs such as f(x) == x * 2, sketches with explicit ?? holes, bounded integer/string/bool hole values, and oracle/test-case verification. It is not a general-purpose production code synthesizer. Treat verified=True as "no counterexample was found within the configured oracle/input search," not as a universal proof that arbitrary generated code is production-safe.

Simulation/fallback paths are separated from production reporting. The synthesize, sketch_synthesize, and verify ops always report completion_state: qualified-draft (a bounded oracle/sampling — and, when Racket is present, a bounded 64-bit Rosette — check is never an unbounded proof), and carry the reliability envelope (completion_state, warning_card, evidence, run_id). LLM-only/fallback/degraded synthesis legs can never raise the result to completion_state: verified; that label is reserved for read-only discovery/metadata ops (e.g. list_capabilities, describe_*). Missing-dependency, unsafe-source, and timeout conditions degrade to blocked-escalated with a stable error code. Residual: full formal/expert-grounded evidence packet is still required before production promotion (component maturity is beta).

When to use:

Synthesising small deterministic functions from simple specifications
Filling sketch holes via the CEGIS loop (Algorithm 1)
Counterexample-driven refinement against an oracle or test cases

Avoid using it for:

Large application features, side-effecting code, network/database/file operations, or framework integration code
Security-critical or regulated workflows without independent review and domain-specific validation
Claims that require full formal proof beyond the bounded validators and solver paths used by this component

Example:

from mvp.cegis import CEGISBlock, CEGISInput

block = CEGISBlock(name="cegis")
result = block.infer(CEGISInput(spec_expr="f(x) == x * 2"))
# result.ok → True; result.value → CEGISOutput with verified program

Works well with: formal_methods, meta_programming, align_csf

Public API¶

`AgencyLevel(IntEnum)`¶

Decreasing value = more programmatic, less LLM dependency.

`CEGISBlock(AIBlock[CEGISInput, CEGISOutput, dict])`¶

Adaptive CEGIS synthesiser.

Field	Type	Default
`name`	`str`	'cegis'
`resource_bounds`	`ResourceBounds \\| None`	None
`usage`	`ResourceUsage`	field(default_factory=ResourceUsage)

Methods:

`infer(data: CEGISInput) -> Result[CEGISOutput]`¶

`synthesize_from_nl(nl_spec: str, oracle_src: str, arg_names: list[str] | None = None, examples: list[tuple[dict, Any]] | None = None, hole_range: Any = None, config: Any = None) -> Result[CEGISOutput]`¶

LLM-native CEGIS (the agentic front-end).

`bias() -> dict`¶

`RunResult`¶

Result of a CEGISEngine.run() call.

Field	Type	Default
`control`	`Control \\| None`	required
`program`	`str`	required
`verified`	`bool`	required
`iterations`	`int`	required
`counterexamples`	`list[dict]`	required
`agency_levels_used`	`list[int]`	required
`unsat`	`bool`	False
`timed_out`	`bool`	False
`synthesis_backend`	`str`	'programmatic'
`rosette_verified`	`bool`	False

`CEGISEngine`¶

CEGIS loop with progressive agency reduction.

Field	Type	Default
`sketch`	`Sketch`	required
`oracle_fn`	`Callable`	required
`arg_names`	`list[str]`	required
`max_iterations`	`int`	20
`hole_lo`	`int`	-32
`hole_hi`	`int`	32
`synthesizer`	`InductiveSynthesizer`	field(default_factory=InductiveSynthesizer)
`validator`	`Validator`	field(default_factory=lambda: Validator(oracle_fn=lambda: None))
`llm_config`	`Any`	None
`agency_start`	`int`	5
`agency_decay`	`int`	1
`max_time_secs`	`float \\| None`	None
`oracle_src`	`str \\| None`	None

Methods:

`run() -> RunResult`¶

Execute Algorithm 1 with progressive LLM agency reduction.

`Hole`¶

A single hole in a sketch.

Field	Type	Default
`id`	`int`	required
`kind`	`HoleKind`	HoleKind.INT
`lo`	`int`	-32
`hi`	`int`	32
`choices`	`tuple[Any, ...]`	()

Methods:

`all_values() -> list[Any]`¶

All valid values for this hole.

`HoleSet`¶

The full set of holes extracted from a sketch.

Field	Type	Default
`holes`	`list[Hole]`	required

Methods:

`n_holes() -> int`¶

`LLMSynthConfig`¶

Config for LLM-assisted synthesis.

Field	Type	Default
`model`	`str`	'ollama/gpt-oss:20b'
`max_tokens`	`int`	1024
`temperature`	`float`	0.2

`LLMFunctionSynthesizer`¶

LLM-driven full-function synthesis with CEGIS counterexample verification.

Constructor:

Parameter	Type	Default
`config`	`LLMSynthConfig`	required

Methods:

`synthesize(description: str, oracle_fn: 'Callable', arg_names: list[str], max_iterations: int = 10, max_time_secs: float = 30.0) -> 'tuple[str | None, bool, list[dict]]'`¶

Generate a function satisfying oracle_fn via LLM + CEGIS verification.

`CEGISInput(BaseModel)`¶

Input to CEGISBlock.

Field	Type	Default
`spec_expr`	`str`	required
`program_template`	`str`	''
`strategy`	`Literal['programmatic', 'structured_llm', 'freeform_llm', 'auto_sketch']`	'programmatic'
`max_iterations`	`int`	10
`domain`	`str`	'general'
`sketch_spec`	`'SketchSpec \\| None'`	None
`natural_spec`	`'NaturalSpec \\| None'`	None

`CounterExample(BaseModel)`¶

A concrete counterexample found during CEGIS verification.

Field	Type	Default
`iteration`	`int`	required
`input_values`	`dict[str, object]`	required
`reason`	`str`	required

`CEGISOutput(BaseModel)`¶

Output from CEGISBlock.

Field	Type	Default
`program`	`str`	required
`verified`	`bool`	required
`iterations`	`int`	required
`counterexamples`	`list[CounterExample]`	Field(default_factory=list)
`strategy_used`	`str`	required
`spec_expr`	`str`	required
`agency_levels_used`	`list[int]`	Field(default_factory=list)
`synthesis_trace`	`list['SynthesisTrace']`	Field(default_factory=list)
`degraded`	`bool`	False
`degradation_reason`	`str`	''
`synthesis_backend`	`str`	'programmatic'
`llm_used`	`bool`	False
`verification_boundary`	`VerificationBoundary`	Field(default_factory=VerificationBoundary)
`optimality`	`OptimalityStamp`	Field(default_factory=OptimalityStamp)

`HoleRange(BaseModel)`¶

Integer range for hole synthesis.

Field	Type	Default
`lo`	`int`	-32
`hi`	`int`	32

`SketchSpec(BaseModel)`¶

Input spec for sketch-based CEGIS (hole-filling mode).

Field	Type	Default
`sketch_src`	`str`	required
`oracle_src`	`str`	required
`hole_range`	`HoleRange`	Field(default_factory=HoleRange)
`max_iterations`	`int`	20
`llm_config`	`LLMSynthConfig \\| None`	None
`agency_start`	`int`	5
`agency_decay`	`int`	1

`SynthesisTrace(BaseModel)`¶

Per-iteration trace entry.

Field	Type	Default
`iteration`	`int`	required
`agency_level`	`int`	required
`control`	`dict[str, int]`	required
`counterexample`	`dict[str, object] \\| None`	required

`NaturalSpec(BaseModel)`¶

Input spec for LLM free-form synthesis (freeform_llm strategy).

Field	Type	Default
`description`	`str`	required
`arg_names`	`list[str]`	required
`oracle_src`	`str \\| None`	None
`test_cases`	`list[dict] \\| None`	None
`llm_config`	`'LLMSynthConfig \\| None'`	None
`max_iterations`	`int`	10
`max_time_secs`	`float`	30.0

`Sketch`¶

A program with holes, ready for synthesis.

Field	Type	Default
`original_src`	`str`	required
`modified_src`	`str`	required
`holes`	`HoleSet`	required
`fn_name`	`str`	'f'

Methods:

`instantiate(control: dict[int, Any]) -> str`¶

Return concrete Python source with all holes filled.

`exec_with(control: dict[int, Any], input_kwargs: dict[str, Any]) -> Any`¶

Execute the filled-in function on input_kwargs.

`from_src(src: str, lo: int = -32, hi: int = 32) -> 'Sketch'`¶

Create Sketch by scanning src for ?? tokens.

`InductiveSynthesizer`¶

Find a control satisfying a set of (input, expected_output) examples.

Field	Type	Default
`max_exhaustive_controls`	`int`	50000

Methods:

`synthesize(sketch: Sketch, examples: list[tuple[dict[str, Any], Any]]) -> Control | None`¶

Return a control that passes ALL examples, or None if UNSAT.

`Validator`¶

Find a counterexample for a candidate program vs an oracle.

Field	Type	Default
`oracle_fn`	`Callable`	required
`n_random`	`int`	200
`seed`	`int`	42

Methods:

`find_counterexample(sketch: Sketch, control: Control, arg_names: list[str], int_range: range = range(-10, 11)) -> dict[str, Any] | None`¶

Return input kwargs where candidate != oracle, or None if verified.

`generate_inputs(arg_names: list[str], int_range: range = range(-10, 11)) -> list[dict[str, Any]]`¶

Generate type-aware test inputs: boundary combos + random sampling.

`CEGISMCPBlock(AIBlock[MCPCEGISInput, MCPCEGISOutput, dict])`¶

27-op CEGIS MCP block: synthesis, sketches, oracles, analysis, metadata.

Field	Type	Default
`name`	`str`	'cegis_mcp'
`state`	`dict \\| None`	None
`db_path`	`str`	':memory:'

Methods:

`infer(data: MCPCEGISInput) -> Result[MCPCEGISOutput]`¶

`MCPCEGISInput(BaseModel)`¶

Field	Type	Default
`op`	`CEGISMCPOp`	required
`spec_expr`	`str`	''
`sketch_src`	`str`	''
`oracle_src`	`str`	''
`candidate_src`	`str`	''
`max_iterations`	`int`	10
`strategy`	`str`	'programmatic'
`domain`	`str`	'general'
`hole_lo`	`int`	-32
`hole_hi`	`int`	32
`agency_start`	`int`	5
`agency_decay`	`int`	1
`type_bias_mode`	`str`	'unrestricted'
`arg_names`	`list[str]`	Field(default_factory=list)
`test_cases`	`list[dict]`	Field(default_factory=list)
`name`	`str`	''
`description`	`str`	''
`result_id`	`str`	''
`result_id_b`	`str`	''
`query`	`str`	''
`verified_only`	`bool`	False
`limit`	`int`	20
`program`	`str`	''
`iterations`	`int`	0
`verified`	`bool`	False
`counterexamples`	`list[dict[str, Any]]`	Field(default_factory=list)
`iteration`	`int`	0
`input_values`	`dict[str, Any]`	Field(default_factory=dict)
`reason`	`str`	''
`metadata`	`dict[str, Any]`	Field(default_factory=dict)

`MCPCEGISOutput(BaseModel)`¶

Field	Type	Default
`op`	`str`	required
`success`	`bool`	False
`result_id`	`str`	''
`result`	`dict[str, Any]`	Field(default_factory=dict)
`results`	`list[dict[str, Any]]`	Field(default_factory=list)
`sketch`	`dict[str, Any]`	Field(default_factory=dict)
`sketches`	`list[dict[str, Any]]`	Field(default_factory=list)
`oracle`	`dict[str, Any]`	Field(default_factory=dict)
`oracles`	`list[dict[str, Any]]`	Field(default_factory=list)
`counterexamples`	`list[dict[str, Any]]`	Field(default_factory=list)
`program`	`str`	''
`verified`	`bool`	False
`iterations`	`int`	0
`strategy_used`	`str`	''
`stats`	`dict[str, Any]`	Field(default_factory=dict)
`suggestions`	`list[str]`	Field(default_factory=list)
`count`	`int`	0
`message`	`str`	''
`error`	`str`	''
`degraded`	`bool`	False
`degradation_reason`	`str`	''
`error_code`	`str`	''
`verification_boundary`	`dict[str, Any] \\| None`	None
`synthesis_backend`	`str`	''
`llm_used`	`bool`	False
`agentic_evidence`	`dict[str, Any]`	Field(default_factory=dict)
`backend_status`	`dict[str, Any]`	Field(default_factory=dict)
`completion_state`	`str`	''
`warning_card`	`str`	''
`evidence`	`dict[str, Any]`	Field(default_factory=dict)
`request_id`	`str`	''
`task_id`	`str`	''
`run_id`	`str`	''

Functions¶

`agency_for_iteration(start: int, iteration: int, decay: int = 1) -> AgencyLevel`¶

Return the agency level for a given iteration.

`all_controls(holes: HoleSet) -> Iterator[Control]`¶

Yield every possible control (Cartesian product of each hole's values).

`random_control(holes: HoleSet, rng: _random.Random | None = None) -> Control`¶

Return a random control (one value per hole within its valid range).

`extract_holes(src: str, lo: int = -32, hi: int = 32) -> tuple[str, HoleSet]`¶

Replace typed ?? tokens with CEGIS_H0, CEGIS_H1, ... left-to-right.

MCP Tools¶

Operation	Source
`synthesize`	cegis_mcp
`sketch_synthesize`	cegis_mcp
`verify`	cegis_mcp
`generate_sketch`	cegis_mcp
`trace`	cegis_mcp
`store_result`	cegis_mcp
`get_result`	cegis_mcp
`list_results`	cegis_mcp
`delete_result`	cegis_mcp
`search_results`	cegis_mcp
`store_sketch`	cegis_mcp
`get_sketch`	cegis_mcp
`list_sketches`	cegis_mcp
`delete_sketch`	cegis_mcp
`update_sketch`	cegis_mcp
`store_oracle`	cegis_mcp
`get_oracle`	cegis_mcp
`list_oracles`	cegis_mcp
`validate_oracle`	cegis_mcp
`delete_oracle`	cegis_mcp
`get_counterexamples`	cegis_mcp
`analyze_failure`	cegis_mcp
`suggest_fix`	cegis_mcp
`compare_results`	cegis_mcp
`stats`	cegis_mcp
`info`	cegis_mcp
`list_patterns`	cegis_mcp
`list_capabilities`	cegis_mcp
`list_algorithm_templates`	cegis_mcp
`describe_algorithm_template`	cegis_mcp
`list_hole_kinds`	cegis_mcp
`describe_type_biases`	cegis_mcp
`list_combinator_registries`	cegis_mcp
`probe_solver_backends`	cegis_mcp
`describe_verification_boundary`	cegis_mcp
`describe_synthesis_backends`	cegis_mcp
`select_algorithm`	cegis_mcp
`preview_composition`	cegis_mcp
`describe_rosette_grammar`	cegis_mcp

Cegis¶

Overview¶

Public API¶

AgencyLevel(IntEnum)¶

CEGISBlock(AIBlock[CEGISInput, CEGISOutput, dict])¶

infer(data: CEGISInput) -> Result[CEGISOutput]¶

synthesize_from_nl(nl_spec: str, oracle_src: str, arg_names: list[str] | None = None, examples: list[tuple[dict, Any]] | None = None, hole_range: Any = None, config: Any = None) -> Result[CEGISOutput]¶

bias() -> dict¶

RunResult¶

CEGISEngine¶

run() -> RunResult¶

Hole¶

all_values() -> list[Any]¶

HoleSet¶

n_holes() -> int¶

LLMSynthConfig¶

LLMFunctionSynthesizer¶

synthesize(description: str, oracle_fn: 'Callable', arg_names: list[str], max_iterations: int = 10, max_time_secs: float = 30.0) -> 'tuple[str | None, bool, list[dict]]'¶

CEGISInput(BaseModel)¶

CounterExample(BaseModel)¶

CEGISOutput(BaseModel)¶

HoleRange(BaseModel)¶

SketchSpec(BaseModel)¶

SynthesisTrace(BaseModel)¶

NaturalSpec(BaseModel)¶

Sketch¶

instantiate(control: dict[int, Any]) -> str¶

exec_with(control: dict[int, Any], input_kwargs: dict[str, Any]) -> Any¶

from_src(src: str, lo: int = -32, hi: int = 32) -> 'Sketch'¶

InductiveSynthesizer¶

synthesize(sketch: Sketch, examples: list[tuple[dict[str, Any], Any]]) -> Control | None¶

Validator¶

find_counterexample(sketch: Sketch, control: Control, arg_names: list[str], int_range: range = range(-10, 11)) -> dict[str, Any] | None¶

generate_inputs(arg_names: list[str], int_range: range = range(-10, 11)) -> list[dict[str, Any]]¶

CEGISMCPBlock(AIBlock[MCPCEGISInput, MCPCEGISOutput, dict])¶

infer(data: MCPCEGISInput) -> Result[MCPCEGISOutput]¶

MCPCEGISInput(BaseModel)¶

MCPCEGISOutput(BaseModel)¶

Functions¶

agency_for_iteration(start: int, iteration: int, decay: int = 1) -> AgencyLevel¶

all_controls(holes: HoleSet) -> Iterator[Control]¶

random_control(holes: HoleSet, rng: _random.Random | None = None) -> Control¶

extract_holes(src: str, lo: int = -32, hi: int = 32) -> tuple[str, HoleSet]¶

MCP Tools¶

`AgencyLevel(IntEnum)`¶

`CEGISBlock(AIBlock[CEGISInput, CEGISOutput, dict])`¶

`infer(data: CEGISInput) -> Result[CEGISOutput]`¶

`synthesize_from_nl(nl_spec: str, oracle_src: str, arg_names: list[str] | None = None, examples: list[tuple[dict, Any]] | None = None, hole_range: Any = None, config: Any = None) -> Result[CEGISOutput]`¶

`bias() -> dict`¶

`RunResult`¶

`CEGISEngine`¶

`run() -> RunResult`¶

`Hole`¶

`all_values() -> list[Any]`¶

`HoleSet`¶

`n_holes() -> int`¶

`LLMSynthConfig`¶

`LLMFunctionSynthesizer`¶

`synthesize(description: str, oracle_fn: 'Callable', arg_names: list[str], max_iterations: int = 10, max_time_secs: float = 30.0) -> 'tuple[str | None, bool, list[dict]]'`¶

`CEGISInput(BaseModel)`¶

`CounterExample(BaseModel)`¶

`CEGISOutput(BaseModel)`¶

`HoleRange(BaseModel)`¶

`SketchSpec(BaseModel)`¶

`SynthesisTrace(BaseModel)`¶

`NaturalSpec(BaseModel)`¶

`Sketch`¶

`instantiate(control: dict[int, Any]) -> str`¶

`exec_with(control: dict[int, Any], input_kwargs: dict[str, Any]) -> Any`¶

`from_src(src: str, lo: int = -32, hi: int = 32) -> 'Sketch'`¶

`InductiveSynthesizer`¶

`synthesize(sketch: Sketch, examples: list[tuple[dict[str, Any], Any]]) -> Control | None`¶

`Validator`¶

`find_counterexample(sketch: Sketch, control: Control, arg_names: list[str], int_range: range = range(-10, 11)) -> dict[str, Any] | None`¶

`generate_inputs(arg_names: list[str], int_range: range = range(-10, 11)) -> list[dict[str, Any]]`¶

`CEGISMCPBlock(AIBlock[MCPCEGISInput, MCPCEGISOutput, dict])`¶

`infer(data: MCPCEGISInput) -> Result[MCPCEGISOutput]`¶

`MCPCEGISInput(BaseModel)`¶

`MCPCEGISOutput(BaseModel)`¶

`agency_for_iteration(start: int, iteration: int, decay: int = 1) -> AgencyLevel`¶

`all_controls(holes: HoleSet) -> Iterator[Control]`¶

`random_control(holes: HoleSet, rng: _random.Random | None = None) -> Control`¶

`extract_holes(src: str, lo: int = -32, hi: int = 32) -> tuple[str, HoleSet]`¶