SemanticVerifier

SemanticVerifier is a formal verification engine for FrameNet Semantic IR in Elixir, leveraging the Z3 SMT Theorem Prover to eliminate dead branches and enforce safety invariants before AST compilation.

This project aims to develop a system that helps ensure an intent is correctly understood whenever a human or a machine produces one.
İnsan ya da makine bir niyet ürettiğinde, bu niyetin doğru anlaşılmasına yardımcı olabilecek bir sistemin geliştirilmesini amaçlıyoruz.

The Hex core includes the complete verification substrate: Semantic IR schema validation, offline FrameNet grounding and Frame-Element bindings, AST/IR normalization, SMT-LIB2 encoding, Z3 solving, counter-example parsing, bounded repair proposals, transition/flow proofs, provenance, fingerprints, proof traces, and domain-error semantics. The optional compiler adapter adds trusted source review, Elixir style checks, and source/code generation; it does not replace or contain the core FrameNet/SMT verifier.

Purpose

SemanticVerifier turns structured semantic intent into an auditable proof pipeline. It checks the IR and its FrameNet grounding, translates safety obligations into SMT-LIB2, asks Z3 for a proof or counter-example, and returns evidence that an application or adapter can inspect before execution. Its goal is to make semantic and state-transition decisions verifiable without coupling the core to an editor, language server, agent provider, blockchain, or user interface.

Development status: SemanticVerifier is still under active development. Do not use it as the sole authorization or safety boundary in production. Before production adoption, pin a reviewed release and independently test the IR contracts, FrameNet manifests, policies, Z3 version, failure handling, resource limits, and any surrounding adapter or execution system. This is especially important for safety-critical, nuclear, medical, energy, industrial-control, critical-infrastructure, financial, or privileged systems.

Rule-first principle

Natural-language input may be a convenient front end, but it is never the authority. LLMs and agents may propose an interpretation, FrameNet mapping, or repair; the versioned contract, schema, FrameNet manifest, policy, and SMT/Z3 proof determine whether that proposal is admissible. Ambiguity, missing evidence, or an unverifiable transition must fail closed rather than being resolved by model confidence.

Key Features

Two-Phase Verification: Structural checking with NimbleOptions, followed by first-order logic proving via Z3.
Zero-Disk Session Pool: In-memory interactive Port pool (z3 -in -smt2) eliminating temporary file I/O.
Dead Code Detection: Identifies unreachable branches and shadowed conditions.
Counter-Example Extraction: Parses SMT (get-model) outputs into structured Elixir maps.
Bounded IR repair proposals: Identifies dead branches and missing preconditions without executing or rewriting source files.
Offline FrameNet grounding: Validates a small, versioned FrameNet 1.7 settlement vocabulary (Commerce_buy, Being_obligated) and typed FE bindings without a live service or natural-language parsing.

Offline FrameNet grounding

SemanticVerifier.FrameNet deliberately embeds a small, versioned vocabulary for the settlement demo. It validates FrameNet frame/FE names and typed operational bindings before Z3 is invoked; it is not a FrameNet API client, corpus browser, lexical-unit resolver, or natural-language WSD component.

Runnable end-to-end examples live in the sibling semantic_verifier_demos project so the Hex package remains a reusable core.

The fixture grounds Being_obligated.Responsible_party/Duty and Commerce_buy.Buyer/Seller/Goods/Money, then verifies the corresponding authorization, balance, and amount preconditions with Z3.

For editor diagnostics, audit records, or generated-code traceability, the opt-in SemanticVerifier.Provenance helper emits a common versioned map for both FrameNet grounding and SemanticVerifier.TransitionVerifier proof entries. It does not alter the existing verifier result or error shapes.

SemanticVerifier.ErrorSemantics.to_record/2 is the complementary opt-in adapter for audit/UI consumers: it converts a verifier error plus optional IR or provenance context into a serializable v1 domain-error record. Unknown error category/cause pairs are explicitly marked unmapped_error rather than silently assigned a semantic meaning.

SemanticVerifier.DomainErrorCatalogue is the public, versioned source of stable domain-error metadata. It currently grounds authorization and AML only from explicit predicates, resource access only for runtime-supported Readable/Writable guards, and OTP supervision only when a transition error identifies a supervision operation frame. Its permitted repair class is policy metadata; it does not change or invoke RepairPlanner.

Trusted source review task

For local contract files you trust enough to execute, run:

mix semantic.review path/to/contract.ex
mix semantic.review --strict path/to/contract.ex

This functionality now lives in the optional semantic_verifier_compiler adapter package. Its task evaluates the supplied source file, then prints compiler diagnostics together with automatic error_semantics and repair_plan records. The default command reports findings and exits successfully; --strict exits nonzero only when semantic verification errors are found, which is useful for CI.

Human approval queue

SemanticVerifier.ApprovalStore is an in-memory OTP service for needs_human_review plan items. A request requires an owner plus evidence, proof, and semantic-record references; it can be approved or rejected by an explicit decision owner and may expire. It records decisions only—approval never auto-applies a repair. Runnable approval scenarios live in semantic_verifier_demos.

Verification fingerprints

SemanticVerifier.Fingerprint.fingerprint/2 produces a SHA-256 fingerprint from canonicalized IR plus an explicit versioned context containing mode, options, catalogue, framenet, encoder, verifier, and solver. It is a pure helper: it does not read solver state, clocks, caches, files, or network data. Missing context is returned as an explicit error.

Quick start (Hex core only)

The following example uses only the semantic_verifier Hex package. You do not need the ATM, agent, X402, MCP, or marketplace demo projects.

First create a small consumer project and install the package:

mix new verifier_example
cd verifier_example

Add the dependency to mix.exs before running mix deps.get:

defp deps do
  [
    {:semantic_verifier, "== 0.2.0-rc.2"}
  ]
end

mix deps.get
iex -S mix

The package requires the Z3 command-line executable; see Requirements.

The two sessions below run directly in IEx and exercise the core verifier.

The two sessions below were run with iex -S mix; runnable application variants are maintained in the sibling semantic_verifier_demos project.

1. Happy path — a valid IR verifies cleanly

The frame declares the preconditions its safety constraint needs, so verification returns {:ok, verified} with no errors and no recovery candidates. The enriched IR adds a "branches" key to every frame and top-level errors/recovery_candidates alongside their atom-keyed counterparts.

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)
{:ok,
 %{
   :errors => [],
   "constraints" => ["Readable(file.txt)"],
   "errors" => [],
   "frames" => [
     %{
       "FE" => %{"Source" => "file.txt"},
       "Preconditions" => ["Exists(file.txt)", "Readable(file.txt)"],
       "branches" => [],
       "frame" => "Reading",
       "id" => "f1"
     }
   ],
   "intent" => "sample_pipeline",
   "recovery_candidates" => []
 }}

2. Violated invariant — counter-example and recovery candidate

The frame reads protected.txt but declares no preconditions, so Readable(protected.txt) cannot be formally proven. The returned %SemanticVerifier.Error{} carries the violated constraint plus a concrete Z3 counter-example model (Readable -> false), and the enriched IR proposes adding the missing precondition — exactly what SemanticVerifier.auto_heal/1 applies.

iex> invalid_ir = %{
...>   "intent" => "violation_test",
...>   "frames" => [
...>     %{"id" => "f1", "frame" => "Reading", "FE" => %{"Source" => "protected.txt"}, "Preconditions" => []}
...>   ],
...>   "constraints" => ["Readable(protected.txt)"]
...> }
iex> {:error, [error | _], enriched_ir} = SemanticVerifier.verify(invalid_ir)
{:error,
 [
   %SemanticVerifier.Error{
     id: "err_39536691",
     category: "IOError",
     cause: "SMT_MODEL_COUNTER_EXAMPLE",
     violated_constraint: "Readable(protected.txt)",
     affected_node: "f1",
     target: nil,
     impact: "Safety invariant 'Readable(protected.txt)' cannot be formally proven.",
     smt_status: :sat_violation_found,
     counter_example: %{
       functions: %{
         "Exists" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true},
         "IsFile" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true},
         "Readable" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: false},
         "Writable" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true}
       },
       raw_model: "(\n  ;; universe for Resource:\n  ;;   Resource!val!0 \n  ;; -----------\n  ;; definitions for universe elements:\n  (declare-fun Resource!val!0 () Resource)\n  ;; cardinality constraint:\n  (forall ((x Resource)) (= x Resource!val!0))\n  ;; -----------\n  (define-fun protected.txt () Resource\n    Resource!val!0)\n  (define-fun IsFile ((x!0 Resource)) Bool\n    true)\n  (define-fun Exists ((x!0 Resource)) Bool\n    true)\n  (define-fun Readable ((x!0 Resource)) Bool\n    false)\n  (define-fun Writable ((x!0 Resource)) Bool\n    true)\n)",
       constants: %{"protected.txt" => "Resource!val!0"}
     }
   }
 ],
 %{
   :errors => [ ... ],
   :recovery_candidates => [
     %{
       reason: "Explicitly enforce 'Readable(protected.txt)' prior to execution",
       action: "AddPrecondition",
       constraint: "Readable(protected.txt)",
       target: "f1",
       confidence: 0.95,
       risk: "Low"
     }
   ],
   "constraints" => ["Readable(protected.txt)"],
   "errors" => [],
   "frames" => [ ... ],
   "intent" => "violation_test",
   "recovery_candidates" => []
 }}

The error id is derived deterministically from the violated constraint. The raw_model string is emitted by Z3 and may vary slightly across Z3 versions. For brevity, the enriched IR above elides the repeated error under :errors/"errors" and the frames (each frame gains "branches" => []); the sibling demo project prints complete runnable output.

Full demonstrations (optional)

The separate semantic_verifier_demos project contains larger integrations:

ATM and OTP state-machine scenarios
FrameNet dialogue and semantic-IR traces
X402/Base Sepolia settlement simulations
agent providers, marketplace discovery, MCP, and YAML contracts

These projects are intentionally not dependencies of the Hex core package. Install the core package first and use the demo repository only when you want to run those end-to-end scenarios.

Requirements

Requires the Z3 SMT Solver CLI:

macOS:brew install z3
Ubuntu/Debian:sudo apt-get install -y z3