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.

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.
• Self-Healing AST Engine: Automatically prunes dead code and synthesizes missing preconditions.

Demo

The two sessions below were run with iex -S mix; the same calls are collected in examples/demo_pipeline.exs.

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" => []); examples/demo_pipeline.exs prints the complete output.

Requirements

Requires the Z3 SMT Solver CLI:

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

Installation

Add semantic_verifier to mix.exs:

def deps do
  [
    {:semantic_verifier, "~> 0.1.0"}
  ]
end