• Alfred Lopez

Solving Non-Deterministic Agent Errors: Graph-Native SMT Formal Verification in AsanagiDB v1.0.3

Why AI agents need deterministic logic bounds, and how Asanagi AMI combines Z3 theorem proving with graph-grounded memory to eliminate hallucinated logic errors.

#formal-verification #z3 #ami #agentic-ai #gremlin #release #v1.0.3

The Problem: Probabilistic Models vs. Deterministic Realities

Large Language Models (LLMs) and autonomous AI agents are inherently probabilistic. While this makes them remarkably creative and flexible, it introduces a dangerous liability when building production software: models cannot guarantee logic constraints.

When an AI agent is tasked with writing code, executing multi-step workflows, or managing backend data, it relies on fuzzy text prompts, code comments, or docstrings to infer rules. This leads to classic agentic failure modes:

Prompt engineering cannot solve this problem. Deterministic systems require deterministic verification.

The Solution: Asanagi AMI (Agentic Memory Infrastructure)

The Asanagi AMI Suite was built to provide AI agents with a deterministic, graph-grounded memory substrate. Instead of relying solely on vector similarity search or loose prompt text, Asanagi AMI grounds agent memory and system architecture inside a high-performance TinkerPop property graph database.

With AsanagiDB v1.0.3, we are introducing Graph-Native Symbolic Logic Verification—combining Z3 formal theorem proving directly with Gremlin graph traversals.

How Does Code Enter the Graph?

A common question is: Does all source code go into the graph database, and how does it get there?

1. Invariants over Implementation (Selective Storage)

You do not dump millions of lines of raw procedural implementation text into AsanagiDB.

Instead, Asanagi AMI focuses on contracts, preconditions, postconditions, and invariants (similar to Design-by-Contract rules or JUnit assertions) alongside structural AST nodes (class hierarchies, function signatures, variable types). Method implementation bodies remain in source files, while the verifiable logic graph lives in AsanagiDB.

2. How Extraction & Ingestion Occur

public class Spaceship
  invariant fuel >= 0;
{
    private long speed = 0;
    private long fuel = 50;

    public void SetSpeed(int s)
    require
        positive_speed: s >= 0;
    ensure
        speed_changed: old speed != speed;
        speed_set: speed == s;
    {
        this.speed = s;
    }

    public void NoChangeSpeed()
    require
        positive_speed: speed >= 0;
    ensure
        speed_unchanged: old speed == speed;
    {
        // No change to speed - should fail the contract
    }

    public void Refuel()
    ensure
        fuel_increased: fuel > old fuel;
    {
        this.fuel = 100;
    }

    public void BadRefuel()
    ensure
        fuel_decreased: fuel < old fuel;
    {
        this.fuel = 25;
    }
}

What Does the Model Look For in Your Code? (Concrete Code Examples)

You do not need to write formal academic Eiffel or Ada syntax to benefit from Graph-Native SMT verification. Mainstream developers (Java, C#, TypeScript, Go, C++) already write contract logic every day—it is expressed across standard language patterns.

When an AI agent analyzes your codebase, the model scans for five everyday constructs:

1. Guard Clauses & Parameter Validation

In C#, defensive guard clauses checking input parameter bounds are automatically extracted into formal SymbolicOp vertices:

public class BankAccount 
{
    public decimal Balance { get; private set; }

    public void Withdraw(decimal amount) 
    {
        // Guard Clause 1: Extracted as SymbolicOp: gt (amount > 0)
        if (amount <= 0) 
            throw new ArgumentOutOfRangeException(nameof(amount), "Amount must be positive.");

        // Guard Clause 2: Extracted as SymbolicOp: gte (Balance >= amount)
        if (Balance < amount) 
            throw new InvalidOperationException("Insufficient funds.");

        Balance -= amount;
    }
}

What Asanagi AMI stores in the graph:

2. Standard Framework Annotations & Null Checks

In Java, Bean Validation annotations and null guards provide immediate declarative bounds:

public class AccountService {
    public void transfer(@NotNull String targetAccount, @Min(1) BigDecimal amount) {
        // Null check: Extracted as SymbolicOp: neq (targetAccount != null)
        Objects.requireNonNull(targetAccount, "Target account is required");
        
        // Value check: Extracted as SymbolicOp: gt (amount > 0)
        if (amount.compareTo(BigDecimal.ZERO) <= 0) {
            throw new IllegalArgumentException("Transfer amount must be positive");
        }

        // Execute business logic...
    }
}

What Asanagi AMI stores in the graph:

3. Unit Test Assertions & Invariants

@Test
void testWithdrawalLeavesValidBalance() {
    Account acc = new Account(100);
    acc.withdraw(30);
    // Postcondition Assertion: Extracted as SymbolicOp: gte (acc.balance >= 0)
    assertTrue(acc.getBalance() >= 0);
}

What Do You Need to Change in Your Code?

Nothing! If you write clean, defensive C#, Java, TypeScript, or Go code with parameter validation, null-checks, or annotations, the model automatically converts those existing safeguards into formal SymbolicOp graph nodes.

How to Get Your AI Agent to Use Graph-Native SMT Verification

Enabling your AI coding assistant (AsanagiLIS, Antigravity, Claude, Cursor, etc.) to use graph-native formal logic verification takes just three simple steps:

1. Connect AsanagiDB via MCP (Model Context Protocol)

AsanagiDB ships with a built-in MCP server (asanagidb-mcp). Simply register AsanagiDB in your agent’s MCP configuration:

{
  "mcpServers": {
    "asanadb": {
      "command": "asanagidb-mcp",
      "args": ["--db-path", "~/.asanagi/memory"]
    }
  }
}

This exposes tools like logic_prove, memory_save, and graph traversals directly to the LLM tool invocation loop.

2. Add System Instructions or Agent Guidelines

Add a short directive to your project’s .agents/rules/ or system prompt instructing the model to consult and persist logic nodes:

# Formal Logic Verification Directive
1. Query Invariants: Before generating or refactoring critical code, query AsanagiDB for connected logic bounds (`SymbolicOp` / `SymbolicVar` nodes).
2. Prove Constraints: Verify candidate math/logic bounds against Z3 using `logic_prove` or `smtProve()`.
3. Persist Logic Vertices: Save new guard clauses, invariants, and validation rules to AsanagiDB via MCP as graph-native logic vertices.

3. Let the Agent Drive the Feedback Loop

Once configured, the interaction cycle happens autonomously during code generation:

[ Developer Prompt ] -> [ Agent Queries AsanagiDB Invariants ]
                                      |
                                      v
[ Agent Generates Code ] -> [ Agent Runs Z3 via logic_prove MCP Tool ]
                                      |
                       +--------------+--------------+
                       |                             |
                 (SAT/Proven)                  (Counterexample)
                       |                             |
                       v                             v
           [ Agent Persists Logic Vertices ]   [ Agent Fixes Code ]

By placing Z3 formal proof tools inside the agent’s MCP loop, the model self-corrects logic errors locally before any code reaches your repository.

Why Do You Need Asanagi AMI if You Already Have JUnit & Guards?

Runtime guards and unit tests are essential, but they leave three critical gaps that AI agents (and human developers) frequently fall into:

1. Unit Tests Test Specific Points; Z3 Proves 100% of the Input Space

A unit test runs testTransfer(100) and testTransfer(0)—testing 2 discrete input points out of billions of possibilities. If an edge case exists at integer overflow boundaries or under specific parameter combinations, unit tests miss it unless a human explicitly thought to write a test case for it.

2. Generation-Time Guardrails vs. Post-Commit CI Failures

Unit tests run in CI after code has been written, compiled, and pushed. If an AI agent generates code that breaks an edge-case guard, you wait 5 minutes for CI to fail, read a log, and ask the model to re-try.

3. Cross-Service & Cross-Repository Invariant Topology

A guard clause in OrderService.java has zero visibility into invariants inside BillingService.cs or InventoryService.go.

Graph-Native Symbolic Logic: “Prove with Z3, Query with Gremlin”

Previously, formal logic expressions (SymbolicExpr) were stored as opaque binary blobs (Yes, SMT was in AsanagiDB very early in the pre-v1.0.0 phase). While an embedded solver like Z3 could verify a blob when prompted, the Gremlin query engine could not inspect or traverse the logic structure inside.

In v1.0.3, AST logic trees are elevated into first-class graph elements (vertices and directional edges):

[ Legacy: Opaque Blob ]
Node(Contract) ---> [Byte Blob: SymbolicExpr] ---> Z3 Solver
                                              (Gremlin cannot query logic)

[ Graph-Native Logic in Asanagi AMI ]
Node(Contract) ---> Edge(asserts) ---> Node(SymbolicOp: '>=')
                                          |-- Edge(left)  --> Node(SymbolicVar: 'balance')
                                          +-- Edge(right) --> Node(SymbolicLit: 0)

The Graph Schema

How Agents Use Graph-Native SMT Verification

By unifying formal verification with property graphs, Asanagi AMI enables three core agentic capabilities:

1. Zero-Hallucination Guardrails

Before an agent generates code or executes an operation, it queries the graph for all formal bounds governing the target module:

// Query all formal invariants constraining the 'balance' variable:
g.V().has('name', 'balance').in('operand').in('asserts')

The agent generates candidate code, and AsanagiDB passes the AST to Z3 via smtProve(). If Z3 returns a counterexample (e.g. balance = -1), AsanagiDB isolates the exact failing vertex path (SymbolicOp: gte, left: balance, right: 0), allowing the agent to fix its code deterministically.

2. Autonomous Refactoring & Impact Analysis

When an agent or developer refactors a shared component, it queries the dependency graph to identify every contract affected across the system. It re-verifies only the impacted subgraphs using Z3, guaranteeing zero silent regressions.

3. Verifiable Cross-Agent Memory (Federation)

In federated deployment topologies (--central), agents publish verified logic nodes. Teammate agents pull these verified logic vertices down, ensuring every agent across the fleet enforces identical safety boundaries.

Get Started with AsanagiDB v1.0.3

AsanagiDB v1.0.3 is available now for macOS (Apple-notarized DMG installer), Linux (tar.gz), and Windows (zip).

Request_Community_License

Get your free license

Community tier — perpetual, no credit card required.