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.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`).