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 viaZ3. - 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