A counterexample-guided engine that learns loop invariants for a small imperative language and checks each candidate with an SMT-backed verifier.
local-first formal-methods-verification small-language-frontend verification-condition-generator candidate-grammar counterexample-guided-learner proof-obligation-reporter
-
Updated
Sep 18, 2026 - Python