Adversum — Formally Proven Code Security

Detect, formally prove, and auto-remediate code vulnerabilities with AI and mathematical certainty.

Comment

Inspiration

Modern software and Web3 ecosystems lose billions every year to preventable code vulnerabilities. While Static Application Security Testing (SAST) and traditional LLM audit tools exist, developers face two crippling issues:

  1. Lethal False Positive Rates: Traditional scanners flood engineers with hundreds of non-exploitable warnings.
  2. Hallucinations without Rigor: General AI models guess vulnerabilities without mathematical guarantees.

We built Adversum to bridge the gap between AI speed and mathematical certainty: an autonomous security engine where NVIDIA Nemotron AI formulates exploit hypotheses, and the Z3 SMT solver formally proves or disproves them with zero false positives.

What It Does

Adversum provides an end-to-end autonomous security pipeline for high-stakes codebases and smart contracts:

  • Instant Rust AST Ingestion: Ultra-fast static indexing and control-flow extraction.
  • Cognitive Vulnerability Hypothesizing: Powered by NVIDIA Nemotron, identifying complex multi-step logical bugs (Reentrancy, Integer Overflows, Access Control bypasses).
  • Z3 BitVec Formal Verification: Every AI finding is converted into a First-Order Logic SMT constraint problem. If the solver returns UNSAT, the finding is discarded as a false positive. If SAT, a concrete mathematical counter-example (exploit payload) is generated.
  • Autonomous Patch Synthesis & Validation: Generates remediation patches and re-runs the formal solver to mathematically certify that the vulnerability has been neutralized.

⚙️ How We Built It

[Source Code] ──▶ [Rust AST Engine] ──▶ [NVIDIA Nemotron AI] │ (Hypotheses) ▼ [Verified Patch] ◀── [Auto-Fix] ◀── Z3 SMT Solver │ SAT: Confirmed Exploit UNSAT: False Positive Dropped Adversum is designed with a high-throughput, multi-stage hybrid pipeline:

1. High-Performance Static Core (Rust)

A native Rust parser builds the Abstract Syntax Tree (AST) and extracts function call graphs, external interaction points, and state mutations in sub-millisecond execution time.

2. Cognitive Reasoning via NVIDIA Nemotron & Nebius

Using NVIDIA Nemotron deployed on Nebius Cloud, the engine reasons over AST semantic slices to identify subtle exploitation vectors, producing formal hypothesis anchors with precise symbolic bounds.

3. Z3 SMT Formal Mathematical Prover

Every hypothesis is translated into symbolic BitVector arithmetic ($\mathbb{Z}_{2^{256}}$) constraints. For an arithmetic overflow check on state variables:

$$\exists x, y \in \text{BitVec}_{256} : (x + y < x) \land \text{Guard}(x, y) = \text{false}$$

For state-machine integrity and reentrancy: $$\mathcal{S}{\text{call}} \xrightarrow{\text{fallback}} \mathcal{S}{\text{exploit}} \implies \text{Invariant}(\mathcal{S}) = \text{false}$$

If the solver proves $\text{UNSAT}$, the issue is guaranteed safe. If $\text{SAT}$, an exact counter-example model is extracted.

4. Real-time SOC & Threat Visualization

A reactive React + TypeScript + Vite + Tailwind CSS dashboard featuring a live Threat Stream, Interactive Attack Graphs, War Room simulation, and one-click PoC reproduction.

Challenges We Faced

  • Bridging LLM Output to First-Order SMT Logic: LLMs generate natural text, but Z3 requires strict mathematical constraints. We created an AST anchoring mechanism that deterministically maps Nemotron's semantic reasoning into Z3 BitVec256 formulas.
  • Eliminating Real-World False Positives: Proving that standard checks-effects-interactions or OpenZeppelin reentrancy guards render contracts provably UNSAT without timing out the SMT solver.
  • End-to-End Latency: Ensuring that the full cycle (AST analysis + LLM inference on Nebius + Z3 solving) executes within seconds for continuous CI/CD integration.

Accomplishments We're Proud Of

  • Zero-Tolerance False Positives: Successfully demonstrated on real test suites (reentrancy_protected.sol formally proven UNSAT, while vulnerable contracts were proven SAT with bit-accurate counter-examples).
  • 100% End-to-End Pipeline: From AST parsing to live interactive UI, automated patching, and mathematical validation.
  • Production-Grade Architecture: 210+ automated tests passing across Python and Rust cores.

What We Learned

  • Formal verification and LLMs are complementary superpowers: LLMs excel at creative vulnerability intuition, while SMT solvers provide unbreakable mathematical truth.
  • High-efficiency inference on Nebius Cloud with NVIDIA Nemotron provides the reasoning depth required for complex multi-function smart contract analysis.

What's Next for Adversum

  • Expanding SMT encoding to Solana (Anchor/Rust) and EVM bytecode directly.
  • GitHub Action integration for automated Pull Request formal certification.
  • Multi-agent autonomous red-team vs. blue-team verification in our simulated War Room arena.

Built With

Share this project:

Updates

Submission history