# z3 Published articles for z3. This is one page of public article previews, not the complete archive. Follow Next page to continue. Summaries are not the original full articles. ## Securing the agentic era: Introducing formal verification for CEL DevFeed: [Securing the agentic era: Introducing formal verification for CEL]() Original publisher: [Read original article]() Author: Google Open Source (noreply@blogger.com) Published: 2026-08-18T18:30:00Z Content type: release Language: en Sources: [Google Open Source Blog]() Topics: [Formal verification](), [Automated reasoning](), [Testing](), [Artificial Intelligence]() Tags: [agent](), [ai](), [ai-agent](), [automated-reasoning](), [cel](), [common-expression-language](), [formal-verification](), [open-source](), [security](), [testing](), [verification](), [z3]() ### AI overview Google's Common Expression Language (CEL) Formal Verification Framework is available for proving the correctness of CEL expressions and policies. Powered by the Z3 theorem prover, it complements heuristic testing by using mathematical proofs to identify logic flaws, equivalence issues, and potentially unsafe policy behavior. ### Source excerpt by Sean Huh, Common Expression Language Team We are rapidly entering an era where AI agents can autonomously draft, refactor, and deploy policies that protect our users and our systems. But this velocity introduces a vital question: How do we trust AI-generated policies? Unit tests may fail to cover the infinite set of possible inputs that occur in production; thus, an AI agent that overfits its policy to existing tests may fail spectacularly in production. To secure automated policy authoring, we must combine heuristic testing with mathematical proofs. We are thrilled to announce the Common Expression Language (CEL) Formal Verification Framework is now available. Powered by the Z3 theorem prover, this framework allows you to prove the correctness of your CEL expressions and policies, serving as the ultimate safety net for the agentic policy. Automated reasoning definitively answers questions like: "Is there any combination of inputs that allows an unapproved request into production?" "Are we absolutely certain this AI-refactored policy matches the original behavior?" "Can a bad actor manipulate this rule to force an evaluation error?" Formal verification establishes mathematical certainty across the infinite spectrum of inputs. Proven policies protect your users and system while giving auditors clear proof of compliance. To see these capabilities in action, watch our video demonstrating how the CEL Verifier REPL catches subtle logic flaws in seconds: Proving rules from the ground up Getting started with formal verification doesn't require learning complex architectures right away. You can evaluate simple standalone CEL expressions to catch edge cases that tests easily miss. (Note: The examples below use our interactive REPL syntax--check out the REPL documentation to follow along!) 1. Catching logic bugs in simple expressions (Equivalence) How do you guarantee a refactored rule behaves identically to the original? Suppose we have a policy that allows ports 80 or 443 ## Optimization Models for Subset Cover DevFeed: [Optimization Models for Subset Cover]() Original publisher: [Read original article]() Published: 2020-10-20T09:00:00Z Content type: article Language: en Sources: [Jeremy Kun]() Topics: [Optimization](), [Code](), [Open Source]() Tags: [article](), [boolean-satisfiability](), [combinatorics](), [integer-programming](), [mathematics](), [optimization](), [programming](), [python](), [smt](), [source](), [subset-cover](), [z3]() ### AI overview This article explores subset covering as a combinatorial optimization problem and compares Integer Linear Programming solvers with Z3, an open-source SMT solver from Microsoft. It defines a generalized formulation for covering all subsets of size l with the fewest subsets of size k. ### Source excerpt In a recent newsletter article I complained about how researchers mislead about the applicability of their work. I gave SAT solvers as an example. People provided interesting examples in response, but what was new to me was the concept of SMT (Satisfiability Modulo Theories), an extension to SAT. SMT seems to have more practical uses than vanilla SAT (see the newsletter for details). I wanted to take some time to explore SMT solvers, and I landed on Z3, an open-source SMT solver from Microsoft. ## Taming a wild nanomite-protected MIPS binary with symbolic execution: No Such Crackme DevFeed: [Taming a wild nanomite-protected MIPS binary with symbolic execution: No Such Crackme]() Original publisher: [Read original article]() Author: Axel "0vercl0k" Souchet & Emilien "tr4nce" Girault Published: 2014-10-12T04:35:00Z Content type: tutorial Language: en Sources: [Diary of a reverse-engineer]() Topics: [Assembly](), [Security](), [debug](), [Linux]() Tags: [assembly](), [debugging](), [intel](), [linux](), [mips](), [nosuchcon](), [reverse-engineering](), [security](), [symbolic-execution](), [z3](), [z3py]() ### AI overview A technical walkthrough of a No Such Con security challenge involving a nanomite-protected MIPS binary. The article introduces the challenge, MIPS fundamentals, debugging setup, and symbolic-execution-based analysis, with two co-authored solution paths. ### Source excerpt As last year, the French conference No Such Con returns for its second edition in Paris from the 19th of November until the 21th of November. And again, the brilliant Eloi Vanderbeken & his mates at Synacktiv put together a series of three security challenges especially for this occasion. Apparently, the ...