SemanticVerifier (semantic_verifier v0.1.0)

Copy Markdown View Source

Top-level facade for Semantic IR formal verification, dead branch analysis, counter-example model parsing, and automated self-healing.

Overview

SemanticVerifier accepts FrameNet Semantic IR maps and executes:

  1. Structural validation via SemanticVerifier.Schema.
  2. SMT-LIB2 generation via SemanticVerifier.Encoder.
  3. Interactive Z3 solving via SemanticVerifier.Pool.
  4. Counter-example extraction via SemanticVerifier.ModelParser.

Examples

iex> ir = %{
...>   "intent" => "sample_pipeline",
...>   "frames" => [
...>     %{"id" => "f1", "frame" => "Reading", "FE" => %{"Source" => "file.txt"}, "Preconditions" => ["Exists(file.txt)", "Readable(file.txt)"]}
...>   ],
...>   "constraints" => ["Readable(file.txt)"]
...> }
iex> {:ok, _verified} = SemanticVerifier.verify(ir)

Summary

Functions

auto_heal(ir_data)

Applies automated self-healing transformations to an enriched IR structure.

verify(ir_data, opts \\ [])

Verifies a Semantic IR map against formal invariants and branch reachability constraints.

Functions

auto_heal(ir_data)

@spec auto_heal(map()) :: map()

Applies automated self-healing transformations to an enriched IR structure.

Prunes unreachable decision branches and synthesizes missing preconditions.

verify(ir_data, opts \\ [])

@spec verify(
  map(),
  keyword()
) :: {:ok, map()} | {:error, [SemanticVerifier.Error.t()], map()}

Verifies a Semantic IR map against formal invariants and branch reachability constraints.

Returns {:ok, verified_ir} on success, or {:error, errors, enriched_ir} on violation.