Packages

semantic_verifier

0.1.1
0.2.0-rc.2 0.1.3 0.1.2 0.1.1 0.1.0

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

HexDocs Report package

Current section

Files

Jump to
Readme
5 Versions
1 Dependency
Dependants
Files
Activity
semantic_verifier README.md
Raw

README.md 

# 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

```