semantic_verifier

# Changelog

All notable changes to this project will be documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [0.2.0-rc.2] - Unreleased

This release candidate supersedes `0.2.0-rc.1` with the documented compatibility boundary and a clean repository layout.

### Documentation
- Clarified that the README quick start uses only the Hex core package and IEx.
- Separated optional ATM, OTP, X402, MCP, agent, and marketplace demonstrations from the core installation path.
- Documented that bounded repair produces verification proposals and does not execute or rewrite source files.

### Breaking changes (`0.1.3` → `0.2.0`)
- The core contract now centers on semantic AST/IR verification. Consumers that relied on permissive or undocumented input shapes from `0.1.3` must validate their IR and schema inputs again.
- FrameNet manifest, frame-element, and binding validation is now an explicit admission step before SMT/Z3 verification; unknown semantic symbols are rejected instead of being treated as opaque data.
- Source review, Elixir style checks, compiler/code-generation behavior, and runnable integrations are no longer part of the Hex core package. They belong in the compiler adapter and demo/application projects.
- Proof, provenance, fingerprint, and audit data are now part of the verification flow, so callers should not assume that a boolean result is the complete result contract.
- Repair remains bounded to verified semantic IR (for example, pruning a Z3-proven dead branch); the core does not silently rewrite source files or apply policy-dependent fixes.

The `0.2.0` minor-version change is intentional: under SemVer for pre-1.0 packages, it communicates that the public core contract changed incompatibly while the package is still pre-release. The `0.1.3` entry below is retained as the last `0.1.x` contract reference.

### Compatibility note
- This release intentionally supersedes the `0.1.x` core contract. The compiler/source-review adapter and runnable integrations remain separate projects.

## [0.1.3] - 2026-08-21

### Fixed
- `Encoder.extract_condition_variables/1` now declares bare predicate and identifier criteria (e.g. `IsAuthorized(user)`) as boolean variables, so shadowed/unreachable branch detection works for symbolic criteria instead of silently failing on Z3 "unknown constant" errors.

### Added
- `examples/concurrent_verification.exs`: 200 concurrent verifications through the persistent Z3 session pool with throughput output.
- `examples/self_healing_pipeline.exs`: full detect → heal → re-verify pipeline with before/after AST.
- `examples/access_control_pipeline.exs`: multi-frame authorization gate scenario with a shadowed branch and missing precondition.
- Regression test for shadowed branches with symbolic criteria.

## [0.1.2] - 2026-08-21

### Added
- `examples/demo_pipeline.exs` with the happy-path and counter-example demo sessions.
- README "Demo" section showing both sessions with their `iex -S mix` outputs.

## [0.1.1] - 2026-08-21

### Added
- Example script under `examples/` demonstrating dead-code detection, self-healing, counter-example extraction, and the happy path.

## [0.1.0] - 2026-08-21

### Added
- Pure Elixir SMT-LIB2 formal verification engine with Z3 SMT Theorem Prover.
- Persistent interactive Z3 Port session pool (`SemanticVerifier.Pool`, `SemanticVerifier.Session`) with in-memory `(reset)` recycling.
- Schema validation layer using `NimbleOptions` (`SemanticVerifier.Schema`).
- Dead-code and shadowed decision branch detection.
- Concrete S-expression counter-example parser for `(get-model)` outputs (`SemanticVerifier.ModelParser`).
- AST-level self-healing transformations (`SemanticVerifier.Healer`).