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.

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