Packages
semantic_verifier
0.2.0-rc.2
Pure Elixir SMT-LIB2 formal verification engine for FrameNet Semantic IR with persistent Z3 session pools.
Current section
Files
Jump to
Current section
Files
semantic_verifier
README.md
README.md
# SemanticVerifier
[](https://github.com/collective-mind/semantic_verifier/actions/workflows/ci.yml)
[](https://hex.pm/packages/semantic_verifier)
[](https://hexdocs.pm/semantic_verifier)
[](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.
> This project aims to develop a system that helps ensure an intent is correctly
> understood whenever a human or a machine produces one.
>
> *İnsan ya da makine bir niyet ürettiğinde, bu niyetin doğru anlaşılmasına
> yardımcı olabilecek bir sistemin geliştirilmesini amaçlıyoruz.*
The Hex core includes the complete verification substrate: Semantic IR schema
validation, offline FrameNet grounding and Frame-Element bindings, AST/IR
normalization, SMT-LIB2 encoding, Z3 solving, counter-example parsing, bounded
repair proposals, transition/flow proofs, provenance, fingerprints, proof
traces, and domain-error semantics. The optional compiler adapter adds trusted
source review, Elixir style checks, and source/code generation; it does not
replace or contain the core FrameNet/SMT verifier.
## Purpose
SemanticVerifier turns structured semantic intent into an auditable proof
pipeline. It checks the IR and its FrameNet grounding, translates safety
obligations into SMT-LIB2, asks Z3 for a proof or counter-example, and returns
evidence that an application or adapter can inspect before execution. Its goal
is to make semantic and state-transition decisions verifiable without coupling
the core to an editor, language server, agent provider, blockchain, or user
interface.
> **Development status:** SemanticVerifier is still under active development.
> Do not use it as the sole authorization or safety boundary in production.
> Before production adoption, pin a reviewed release and independently test
> the IR contracts, FrameNet manifests, policies, Z3 version, failure handling,
> resource limits, and any surrounding adapter or execution system. This is
> especially important for safety-critical, nuclear, medical, energy,
> industrial-control, critical-infrastructure, financial, or privileged systems.
## Rule-first principle
Natural-language input may be a convenient front end, but it is never the
authority. LLMs and agents may propose an interpretation, FrameNet mapping, or
repair; the versioned contract, schema, FrameNet manifest, policy, and SMT/Z3
proof determine whether that proposal is admissible. Ambiguity, missing
evidence, or an unverifiable transition must fail closed rather than being
resolved by model confidence.
---
## 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.
* **Bounded IR repair proposals:** Identifies dead branches and missing preconditions without executing or rewriting source files.
* **Offline FrameNet grounding:** Validates a small, versioned FrameNet 1.7 settlement vocabulary (`Commerce_buy`, `Being_obligated`) and typed FE bindings without a live service or natural-language parsing.
### Offline FrameNet grounding
`SemanticVerifier.FrameNet` deliberately embeds a small, versioned vocabulary for the
settlement demo. It validates FrameNet frame/FE names and typed operational bindings
before Z3 is invoked; it is **not** a FrameNet API client, corpus browser, lexical-unit
resolver, or natural-language WSD component.
Runnable end-to-end examples live in the sibling `semantic_verifier_demos`
project so the Hex package remains a reusable core.
The fixture grounds `Being_obligated.Responsible_party`/`Duty` and
`Commerce_buy.Buyer`/`Seller`/`Goods`/`Money`, then verifies the corresponding
authorization, balance, and amount preconditions with Z3.
For editor diagnostics, audit records, or generated-code traceability, the opt-in
`SemanticVerifier.Provenance` helper emits a common versioned map for both
FrameNet grounding and `SemanticVerifier.TransitionVerifier` proof entries.
It does not alter the existing verifier result or error shapes.
`SemanticVerifier.ErrorSemantics.to_record/2` is the complementary opt-in
adapter for audit/UI consumers: it converts a verifier error plus optional IR
or provenance context into a serializable v1 domain-error record. Unknown
error category/cause pairs are explicitly marked `unmapped_error` rather than
silently assigned a semantic meaning.
`SemanticVerifier.DomainErrorCatalogue` is the public, versioned source of
stable domain-error metadata. It currently grounds authorization and AML only
from explicit predicates, resource access only for runtime-supported
`Readable`/`Writable` guards, and OTP supervision only when a transition error
identifies a supervision operation frame. Its permitted repair class is policy
metadata; it does not change or invoke `RepairPlanner`.
### Trusted source review task
For local contract files you trust enough to execute, run:
```bash
mix semantic.review path/to/contract.ex
mix semantic.review --strict path/to/contract.ex
```
This functionality now lives in the optional `semantic_verifier_compiler`
adapter package. Its task evaluates the supplied source file, then prints compiler diagnostics together with automatic
`error_semantics` and `repair_plan` records. The default command reports
findings and exits successfully; `--strict` exits nonzero only when semantic
verification errors are found, which is useful for CI.
### Human approval queue
`SemanticVerifier.ApprovalStore` is an in-memory OTP service for
`needs_human_review` plan items. A request requires an owner plus evidence,
proof, and semantic-record references; it can be approved or rejected by an
explicit decision owner and may expire. It records decisions only—approval
never auto-applies a repair. Runnable approval scenarios live in
`semantic_verifier_demos`.
### Verification fingerprints
`SemanticVerifier.Fingerprint.fingerprint/2` produces a SHA-256 fingerprint
from canonicalized IR plus an explicit versioned context containing `mode`,
`options`, `catalogue`, `framenet`, `encoder`, `verifier`, and `solver`.
It is a pure helper: it does not read solver state, clocks, caches, files, or
network data. Missing context is returned as an explicit error.
---
## Quick start (Hex core only)
The following example uses only the `semantic_verifier` Hex package. You do not
need the ATM, agent, X402, MCP, or marketplace demo projects.
First create a small consumer project and install the package:
```bash
mix new verifier_example
cd verifier_example
```
Add the dependency to `mix.exs` before running `mix deps.get`:
```elixir
defp deps do
[
{:semantic_verifier, "== 0.2.0-rc.2"}
]
end
```
```bash
mix deps.get
iex -S mix
```
The package requires the Z3 command-line executable; see [Requirements](#requirements).
The two sessions below run directly in IEx and exercise the core verifier.
The two sessions below were run with `iex -S mix`; runnable application variants
are maintained in the sibling `semantic_verifier_demos` project.
### 1. Happy path — a valid IR verifies cleanly
The frame declares the preconditions its safety constraint needs, so verification returns `{:ok, verified}` with no errors and no recovery candidates. The enriched IR adds a `"branches"` key to every frame and top-level `errors`/`recovery_candidates` alongside their atom-keyed counterparts.
```elixir
iex> ir = %{
...> "intent" => "sample_pipeline",
...> "frames" => [
...> %{
...> "id" => "f1",
...> "frame" => "Reading",
...> "FE" => %{"Source" => "file.txt"},
...> "Preconditions" => ["Exists(file.txt)", "Readable(file.txt)"]
...> }
...> ],
...> "constraints" => ["Readable(file.txt)"]
...> }
iex> {:ok, verified} = SemanticVerifier.verify(ir)
{:ok,
%{
:errors => [],
"constraints" => ["Readable(file.txt)"],
"errors" => [],
"frames" => [
%{
"FE" => %{"Source" => "file.txt"},
"Preconditions" => ["Exists(file.txt)", "Readable(file.txt)"],
"branches" => [],
"frame" => "Reading",
"id" => "f1"
}
],
"intent" => "sample_pipeline",
"recovery_candidates" => []
}}
```
### 2. Violated invariant — counter-example and recovery candidate
The frame reads `protected.txt` but declares no preconditions, so `Readable(protected.txt)` cannot be formally proven. The returned `%SemanticVerifier.Error{}` carries the violated constraint plus a concrete Z3 counter-example model (`Readable -> false`), and the enriched IR proposes adding the missing precondition — exactly what `SemanticVerifier.auto_heal/1` applies.
```elixir
iex> invalid_ir = %{
...> "intent" => "violation_test",
...> "frames" => [
...> %{"id" => "f1", "frame" => "Reading", "FE" => %{"Source" => "protected.txt"}, "Preconditions" => []}
...> ],
...> "constraints" => ["Readable(protected.txt)"]
...> }
iex> {:error, [error | _], enriched_ir} = SemanticVerifier.verify(invalid_ir)
{:error,
[
%SemanticVerifier.Error{
id: "err_39536691",
category: "IOError",
cause: "SMT_MODEL_COUNTER_EXAMPLE",
violated_constraint: "Readable(protected.txt)",
affected_node: "f1",
target: nil,
impact: "Safety invariant 'Readable(protected.txt)' cannot be formally proven.",
smt_status: :sat_violation_found,
counter_example: %{
functions: %{
"Exists" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true},
"IsFile" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true},
"Readable" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: false},
"Writable" => %{parameters: [["x!0", "Resource"]], return_type: "Bool", interpretation: true}
},
raw_model: "(\n ;; universe for Resource:\n ;; Resource!val!0 \n ;; -----------\n ;; definitions for universe elements:\n (declare-fun Resource!val!0 () Resource)\n ;; cardinality constraint:\n (forall ((x Resource)) (= x Resource!val!0))\n ;; -----------\n (define-fun protected.txt () Resource\n Resource!val!0)\n (define-fun IsFile ((x!0 Resource)) Bool\n true)\n (define-fun Exists ((x!0 Resource)) Bool\n true)\n (define-fun Readable ((x!0 Resource)) Bool\n false)\n (define-fun Writable ((x!0 Resource)) Bool\n true)\n)",
constants: %{"protected.txt" => "Resource!val!0"}
}
}
],
%{
:errors => [ ... ],
:recovery_candidates => [
%{
reason: "Explicitly enforce 'Readable(protected.txt)' prior to execution",
action: "AddPrecondition",
constraint: "Readable(protected.txt)",
target: "f1",
confidence: 0.95,
risk: "Low"
}
],
"constraints" => ["Readable(protected.txt)"],
"errors" => [],
"frames" => [ ... ],
"intent" => "violation_test",
"recovery_candidates" => []
}}
```
> The error `id` is derived deterministically from the violated constraint. The `raw_model` string is emitted by Z3 and may vary slightly across Z3 versions. For brevity, the enriched IR above elides the repeated error under `:errors`/`"errors"` and the frames (each frame gains `"branches" => []`); the sibling demo project prints complete runnable output.
## Full demonstrations (optional)
The separate `semantic_verifier_demos` project contains larger integrations:
* ATM and OTP state-machine scenarios
* FrameNet dialogue and semantic-IR traces
* X402/Base Sepolia settlement simulations
* agent providers, marketplace discovery, MCP, and YAML contracts
These projects are intentionally not dependencies of the Hex core package.
Install the core package first and use the demo repository only when you want
to run those end-to-end scenarios.
---
## Requirements
Requires the **Z3 SMT Solver** CLI:
* **macOS:** `brew install z3`
* **Ubuntu/Debian:** `sudo apt-get install -y z3`
---