NOMOS-VANTAGE

A Neural-Symbolic Chrome Extension fusing Gemini Live's vision with Z3 mathematical logic to physically block catastrophic cloud infrastructure mistakes in real-time.

Comment

🛡️ Inspiration: The Hallucination Problem in Cloud Security

A single misclick in a cloud console—like exposing an AWS S3 bucket or a GCP database to the public—can cost an enterprise millions of dollars in data breaches.

Currently, the industry relies on probabilistic AI agents to suggest security fixes. But probabilistic AI hallucinates. You cannot trust a purely neural network to govern deterministic cloud infrastructure. We realized that for an AI agent to truly act as a security guard, it needed a mathematical "brain" that operates with absolute certainty. We were inspired to build NOMOS-VANTAGE, a Neuro-Symbolic AI agent that moves us from AI that suggests to AI that mathematically protects.

⚙️ What it does

NOMOS-VANTAGE is a real-time, zero-trust UI Navigator agent. It physically paralyzes a web browser before a human engineer can execute a catastrophic cloud misconfiguration.

  1. Perception: A custom Chrome Extension streams the visual state of the AWS/GCP console to the backend.
  2. Cognition: Gemini 2.0 Multimodal Live extracts the user's intent (e.g., "User is attempting to click 'Make Public' on a Production bucket").
  3. Verification: Before the click registers, a Microsoft Z3 SMT Solver runs a formal mathematical proof.
  4. Enforcement: If the action violates security axioms, the extension executes a "Sticky DOM Lockdown," physically hijacking the e.preventDefault() layer so the mouse click fails. Gemini then autonomously executes a tool call to revert the UI state and warns the user out loud.

🏗️ How we built it

We architected NOMOS-VANTAGE as a hybrid Neuro-Symbolic system, bringing together the best of neural perception and deterministic logic:

  • The Eyes (Chrome Extension & WebRTC): We built a browser extension that captures DOM events and visual tab streams, acting as our UI Navigator interface.
  • The Neural Heart (Gemini 2.0 Multimodal Live API): We utilized Gemini 2.0 to rapidly process the visual JSON state and voice inputs. It acts as the translation layer between human UI interactions and strict machine logic.
  • The Symbolic Brain (Z3 SMT Solver): We built a formal verification engine in Python using Microsoft Z3.
  • The Enterprise Backend (FastAPI & Google Cloud): The async engine runs on FastAPI (optimized with uvloop). To satisfy SOC2 compliance, every intercepted threat and its corresponding mathematical proof is logged asynchronously to Google Cloud Firestore.

🧮 The Mathematics of Security (Formal Verification)

To eliminate AI hallucinations, we translate the visual UI state extracted by Gemini into First-Order Logic formulas that the Z3 SMT solver can evaluate.

Let $S$ represent the state of a cloud resource, $E(S)$ be its environment tag, and $V(S)$ be its network visibility. We define our core enterprise safety axiom as:

$$\Phi_{safe} \equiv \forall S \big(E(S) = \text{Prod} \implies V(S) \neq \text{Public} \big)$$

When Gemini extracts a user intent to change the state to $S'$, the Z3 solver does not just guess if it is safe. It checks the satisfiability (SAT) of the negation of our safety axiom against the proposed state:

$$\text{Check: } SAT\big( (E(S') = \text{Prod}) \land (V(S') = \text{Public}) \big)$$

If the Z3 solver returns UNSAT, the state is mathematically safe. If it returns SAT, it proves a catastrophic violation is about to occur. This deterministic proof is what triggers our UI Navigator to lock down the browser's DOM.

🧗 Challenges we ran into

  • Sub-50ms Latency Requirements: Paralyzing a browser before a user's mouse click finishes requires extreme speed. We had to heavily optimize our FastAPI backend using orjson and Bounded ThreadPoolExecutors to ensure the Gemini-to-Z3 pipeline executed in under 200ms.
  • The Final-Hour IAM Lockout: Our architecture includes a fully written, SOC2-compliant logging system using Google Cloud Firestore. However, at 3:00 AM on submission night, we encountered a GCP IAM role propagation delay that threw 403 Permission Denied errors on our Service Account. We had to engineer a rapid "God Mode" bypass key to successfully force the database write and establish our cloud audit trail right before the deadline.

🏆 Accomplishments that we're proud of

  • Successfully integrating the Gemini Multimodal Live API not just as a chatbot, but as an active UI Navigator that physically controls DOM execution.
  • Bridging the gap between LLMs (probabilistic) and SMT Solvers (deterministic).
  • Achieving real-time WebRTC streaming and successfully logging complex mathematical strings to Google Cloud Firestore under extreme time pressure.

🧠 What we learned

We learned that the future of AI in enterprise software isn't just making LLMs bigger; it's pairing them with deterministic systems. The combination of Gemini's incredible visual perception with the unforgiving logic of Z3 creates a new class of software: Hybrid AI that can be trusted with mission-critical infrastructure.

🚀 What's next for NOMOS-VANTAGE

  • Multi-Cloud Axioms: Expanding the Z3 logic engine to support complex IAM role hierarchies in Azure and GCP.
  • CI/CD Integration: Moving the agent beyond the browser to intercept unsafe Terraform and Pulumi deployments in GitHub Actions.
  • Full Cloud Run Deployment: Scaling the WebSockets backend entirely on GCP to offer NOMOS-VANTAGE as an enterprise SaaS.

Built With

Share this project:

Updates