Changelog

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

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

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