# semantic_verifier v0.1.2 - Table of Contents

> Pure Elixir SMT-LIB2 formal verification engine for FrameNet Semantic IR with persistent Z3 session pools.

## Pages

- [SemanticVerifier](readme.md)
- [Changelog](changelog.md)

- Guides
  - [Architecture &amp; Formal SMT Proving](architecture.md)
  - [Counter-Examples &amp; Model Extraction](counter_examples.md)
  - [Self-Healing Engine](self_healing.md)

## Modules

- [SemanticVerifier.Application](SemanticVerifier.Application.md)

- Core Facade
  - [SemanticVerifier](SemanticVerifier.md): Top-level facade for Semantic IR formal verification, dead branch analysis,
counter-example model parsing, and automated self-healing.

- SMT Engine &amp; Session Pool
  - [SemanticVerifier.Encoder](SemanticVerifier.Encoder.md): Encodes Semantic IR constraints, axioms, and branch criteria into SMT-LIB2 s-expressions.

  - [SemanticVerifier.Pool](SemanticVerifier.Pool.md): Lightweight connection pool managing persistent Z3 Session workers with non-blocking checkout.

  - [SemanticVerifier.Session](SemanticVerifier.Session.md): Stateful GenServer managing a single persistent interactive Z3 Port process (`z3 -in -smt2`).

  - [SemanticVerifier.Solver](SemanticVerifier.Solver.md): Resolves SMT queries via the persistent connection pool or standalone session fallback.

- Verification &amp; Transformation
  - [SemanticVerifier.Error](SemanticVerifier.Error.md): Standardized struct representing formal verification violations found by Z3.
Includes concrete counter-example models when constraints are violated.

  - [SemanticVerifier.Healer](SemanticVerifier.Healer.md): Transforms Semantic IR structures by pruning dead branches and injecting recovery preconditions.

  - [SemanticVerifier.ModelParser](SemanticVerifier.ModelParser.md): S-expression tokenizer and parser for Z3 `(get-model)` outputs.
Extracts concrete counter-example variable valuations and function interpretations.

  - [SemanticVerifier.Schema](SemanticVerifier.Schema.md): Schema definitions and validators for Semantic IR structures powered by NimbleOptions.
Ensures strict structural integrity before passing AST/IR to Z3 formal verifiers.

