# SemanticVerifier

[![CI](https://github.com/collective-mind/semantic_verifier/actions/workflows/ci.yml/badge.svg)](https://github.com/collective-mind/semantic_verifier/actions/workflows/ci.yml)
[![Hex.pm](https://img.shields.io/hexpm/v/semantic_verifier.svg)](https://hex.pm/packages/semantic_verifier)
[![Hex Docs](https://img.shields.io/badge/hex-docs-purple.svg)](https://hexdocs.pm/semantic_verifier)
[![License](https://img.shields.io/badge/license-Apache%202.0-blue.svg)](https://github.com/collective-mind/semantic_verifier/blob/main/LICENSE)

**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`:

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