v0.1.0 — Initial Release

??? VeriFix v0.1.0 ? Initial Release

VeriFix is a neurosymbolic automated code vulnerability and bug patcher combining generative LLM synthesis with Microsoft Z3 SMT formal theorem proving.

? Key Features

• Dual-Engine CEGIS Loop: Orchestrates generative patch synthesis with formal verification in a Counterexample-Guided Inductive Synthesis loop.
• SMT Verification Conditions (VCGen): Symbolically executes Python functions across all execution paths, translating AST semantics into first-order logic formulas.
• Concrete Counterexample Extraction: Automatically extracts concrete failure models (e.g., balance=0, amount=1) to guide prompt self-correction without hallucinated patches.
• Safety Invariant Checkers: Out-of-the-box checking for Zero Division, Array Out-of-Bounds, NoneType Dereference, and 32-bit Integer Overflow.
• Formal Contract System: Native support for @requires, @ensures, and invariants via both docstring tags and decorators.
• Full CLI Suite: Interactive verifix demo, static verifix verify, and automated verifix patch.
• Exhaustive Formal Test Suite: 45+ unit and integration tests formally verified.