Dev Nag

Dev Nag

I work on AI assurance: making what AI systems produce and claim checkable by someone who has no reason to trust them.

My recent research used AI systems to prove new lower bounds for depth-two threshold circuits. Each main result is released with a Lean 4 proof that states exactly which published results it assumes and what the machine checks.

I've also spent almost three decades building systems that people rely on. I was co-founder, CTO and CISO of Wavefront, a cloud monitoring company acquired by VMware. At VMware I founded Project Magna, which became vRealize AI Cloud and applied reinforcement learning to infrastructure under operational guardrails. I'm now the founder and CEO of QueryPal, which runs AI agents in production for enterprise support and goes through annual SOC 2 examinations.

What assurance means in my work

AI can now produce proofs, code and research claims faster than people can review them. The bottleneck is no longer generating the work. It is establishing what the work actually shows. I treat each result as a claim that should come with evidence a skeptical reader can check.

The thread is older than the circuit papers. My first papers, written in 2003–2005 with UCSF's Biosystems Group, asked how to validate automated models when automation reduces direct oversight. At Wavefront I was CISO as well as CTO. At VMware, our reinforcement-learning controllers were designed to operate under safety constraints and administrator oversight. At QueryPal I work directly on the controls and evidence for annual SOC 2 examinations.

State the claim exactly

Name the class, the resource being counted, the quantifiers and the error regime. A result that is narrower than its headline is a different result.

Show the trust boundary

Every formal proof lists the published statements it assumes and the axioms it uses. Source-mapping pages put each published sentence beside its Lean transcription.

Check what can be checked

Lean's kernel checks the derivation. Comparator checks the proof against a fixed challenge statement in a sandbox, so the target cannot drift.

Correct in the open

Every version stays public. When building a formalization exposed a scope problem in one imported lemma, I replaced that input, repaired the affected proofs and documented the change.

A checked proof shows that a statement follows from its assumptions. Whether the statement is the right one, and whether each assumption matches its source, still takes judgment. That is why both are published beside the proof.

Questions I'm working on

These are open questions, not results.

Research: lower bounds for threshold circuits

Dark step chart of the best known lower-bound exponents for depth-two threshold circuits from 2016 to 2026. Gates: Kane–Williams 2016 n^1.5; Tamaki 2016 n^2/polylog; Chen–Tal–Wang March 2026 n^(5/2−ε); Dev Nag October 2026 n^3/polylog for SYM∘THR, Lean-checked. Wires: n^5/2 from Kane–Williams 2016, unchanged for a decade; Dev Nag August 2026 n^3/polylog; Dev Nag September 2026 n^(7/2)/polylog, on a linear time axis.
Gate and wire lower bounds for depth-two threshold circuits sat for a decade, then moved in 2026. The highlighted points are my preprints; the Lean proofs are listed below. The exponents ignore polylogarithmic factors, and the results differ in circuit class and hardness type. Vector version (SVG).

These papers study how large a depth-two threshold circuit must be to compute a hard function. The wire papers build on the framework of Chen, Tal and Wang. The work also draws on the restriction method of Kane and Williams and on Williams's algorithmic method. All are open access under CC BY 4.0.

Gates and wires are different measures. A circuit with G gates has at most about nG wires. A bound of n3 gates therefore implies only n3 wires, and a bound of n7/2 wires implies only about n5/2 gates. The results below are not ranked by exponent.

  1. Almost-Everywhere Near-Cubic Gate Lower Bounds for SYM∘THR Circuits#

    Dev Nag · Version 3, October 2026 (first posted October 7, 2026) · Zenodo

    • Main theorem proved in Lean
    • Gates

    How many threshold gates does a depth-two circuit need when its output gate may compute any symmetric function of the gates below it? This paper raises the gate exponent for these SYM∘THR circuits from Chen–Tal–Wang's 5/2 − ε to 3, up to logarithmic factors. A single language in ENP disagrees on a constant fraction of inputs with every such circuit of about n3/polylog n gates, at every sufficiently large input length. The key idea is to reconstruct exact local score distributions, so an arbitrary symmetric output can be evaluated without approximating it.

    Scope: symmetric output gates only. It does not give the same gate bound for general THR∘THR. The guarantee is constant error, not vanishing correlation.

    Formal proof: the main theorem, proved in Lean from seven published statements, using only Lean's three standard axioms and checked against a fixed challenge statement with Comparator.

    BibTeX 
    @misc{nag2026nearcubicgates,
  author    = {Nag, Dev},
  title     = {Almost-Everywhere Near-Cubic Gate Lower Bounds
               for {SYM}$\circ${THR} Circuits},
  year      = {2026},
  publisher = {Zenodo},
  version   = {3},
  doi       = {10.5281/zenodo.23224159},
  url       = {https://doi.org/10.5281/zenodo.23224159}
}

  2. Almost-Everywhere Near-Cubic Wire Lower Bounds for SYM∘THR and THR∘THR#

    Dev Nag · Version 3, October 16, 2026 (first posted August 17, 2026) · Zenodo · ECCC TR26-167

    • Theorem 2.5 proved in Lean
    • Wires

    This paper counts wires rather than gates and proves almost-everywhere near-cubic lower bounds for depth-two threshold circuits. A single language in ENP has agreement below 1/2 + n−c with every SYM∘THR circuit of about n3/log10 n wires and every THR∘THR circuit of about n3/log12 n wires, at every sufficiently large length. At any fixed advantage, the logarithmic losses drop to log5 n and log9 n. It builds on Chen, Tal and Wang's restriction-and-analysis framework and charges only the gates that touch the live variables.

    Formal proof: Theorem 2.5, the fixed-advantage result, proved in Lean from nine published statements. The inverse-polynomial-correlation headline (Theorem 2.3) is not formalized.

    Revision history: version 3 takes its short PCP from Murray and Williams in place of an earlier imported lemma. Earlier versions and the public discussion are on ECCC.

    BibTeX 
    @misc{nag2026nearcubicwires,
  author    = {Nag, Dev},
  title     = {Almost-Everywhere Near-Cubic Wire Lower Bounds
               for {SYM}$\circ${THR} and {THR}$\circ${THR}},
  year      = {2026},
  publisher = {Zenodo},
  version   = {3},
  doi       = {10.5281/zenodo.21984711},
  url       = {https://doi.org/10.5281/zenodo.21984711},
  note      = {Earlier version: ECCC TR26-167}
}

  3. Wire–Correlation Tradeoffs at Exponent 7/2 for Depth-Two Threshold Circuits#

    Dev Nag · Version 1, September 15, 2026 · Zenodo

    • Theorem 1.1, row B, proved in Lean
    • Revision in preparation
    • Wires

    Measured by wires, this paper raises the exponent for almost-everywhere correlation bounds against THR∘THR and SYM∘THR circuits from 3 to 7/2, up to logarithmic factors. Its main technique partitions the input cube into products of Hamming-code stars. A threshold gate is then charged only for genuinely mixed dependence on the two halves of each cell. One-sided behavior, however complicated, is absorbed exactly.

    Formal proof: row B of Theorem 1.1 (c = 1/8, KT = 11/2, KS = 9/2), proved in Lean from nine published statements. The full parameterized theorem and the other rows are not formalized.

    Status: version 1, and the Lean proof's assumptions, use an imported PCP lemma that version 3 of the near-cubic wire paper replaces. A matching revision is in preparation.

    BibTeX 
    @misc{nag2026wireseven,
  author    = {Nag, Dev},
  title     = {Wire--Correlation Tradeoffs at Exponent 7/2
               for Depth-Two Threshold Circuits},
  year      = {2026},
  publisher = {Zenodo},
  version   = {1},
  doi       = {10.5281/zenodo.22774130},
  url       = {https://doi.org/10.5281/zenodo.22774130}
}

  4. Wire-Charged Restrictions: Touching and the Root-Fan-In Frontier#

    Dev Nag · Version 1.0, September 5, 2026 · Zenodo

    • Wires

    This note introduces touching, a wire-sensitive accounting principle for random restrictions. If a restriction leaves k variables live, the expected number of touched bottom gates is at most kW/n for a circuit with W wires, and a good live set can be found deterministically. Combined with an extension of the Chen–Tal–Wang pipeline, it gives a worst-case, infinitely-often n3−ε wire lower bound for THR∘THR. It also introduces the root-fan-in measure Σi√fi.

    BibTeX 
    @misc{nag2026wirecharged,
  author    = {Nag, Dev},
  title     = {Wire-Charged Restrictions: Touching and the
               Root-Fan-In Frontier},
  year      = {2026},
  publisher = {Zenodo},
  version   = {1.0},
  doi       = {10.5281/zenodo.22382523},
  url       = {https://doi.org/10.5281/zenodo.22382523}
}

  5. Almost-Everywhere Near-n5/2 Gate Lower Bounds for SYM∘THR and THR∘THR#

    Dev Nag · Version 1.0, August 19, 2026 · Zenodo

    • Superseded for symmetric tops
    • Gates

    This paper gives an explicit polylogarithmic approach to Chen–Tal–Wang's exponent-5/2 boundary. A single language in ENP requires more than about n5/2/log9/2 n gates for SYM∘THR circuits and n5/2/log9 n gates for THR∘THR circuits, at every sufficiently large length.

    Status: for symmetric output gates, superseded by the near-cubic gate paper above. The posted proof uses the imported PCP lemma that later versions of these papers replace.

    BibTeX 
    @misc{nag2026nearfivehalves,
  author    = {Nag, Dev},
  title     = {Almost-Everywhere Near-$n^{5/2}$ Gate Lower Bounds
               for {SYM}$\circ${THR} and {THR}$\circ${THR}},
  year      = {2026},
  publisher = {Zenodo},
  version   = {1.0},
  doi       = {10.5281/zenodo.22005389},
  url       = {https://doi.org/10.5281/zenodo.22005389}
}

Earlier research: automated modeling and medical informatics

With UCSF's Biosystems Group (C. Anthony Hunt and Glen E. P. Ropella), on validating automated models against experimental evidence; and at Stanford, on the Stanford Health Information Network for Education (SHINE), integrating medical information into clinical decision support.

  1. Similarity Measures and Validation in Automated Modeling

    D. A. Nag, G. E. P. Ropella and C. A. Hunt · Huntsville Simulation Conference, 2005

    How to assess models when automation reduces direct experimenter oversight: similarity measures, validation and a formal framework for automated modeling.

  2. Using Heuristic Models to Bridge the Gap Between Analytic and Experimental Models in Biology

    G. E. P. Ropella, C. A. Hunt and D. A. Nag · Agent-Directed Simulation Symposium, 2005, pp. 182–190

  3. Similarity Measures for Automated Comparison of In Silico and In Vitro Experimental Results

    G. E. P. Ropella, D. A. Nag and C. A. Hunt · IEEE Engineering in Medicine and Biology Society, 2003, pp. 2933–2936

  4. New Paradigms for Medical Decision Support and Education: The Stanford Health Information Network for Education

    P. Godin et al., including D. Nag · Topics in Health Information Management 20(2), 1999, pp. 1–14

  5. A New Instrument for Medical Decision Support and Education: The Stanford Health Information Network for Education

    P. Godin et al., including D. Nag · Hawaii International Conference on System Sciences, 1999

  6. The Stanford Health Information Network for Education: Integrated Information for Decision Making and Learning

    P. R. Hubbs et al., including D. Nag · AMIA Annual Fall Symposium, 1997, pp. 505–508

How the 2026 papers were made

I used generative AI tools from Anthropic (Claude) and OpenAI (ChatGPT and Codex) substantively throughout this work: for exploratory proof search and parameter selection, drafting and revision, literature navigation and source comparison, adversarial review, and the Lean formalizations. Their review passes are not independent human validation. I chose the research targets and the arguments that were kept. I take responsibility for the claims, proofs, originality and citations. No model is an author.

Lean proofs

Each repository builds with a pinned toolchain and prints the proved statement, its exact list of assumed published results, and its axioms (exactly propext, Classical.choice and Quot.sound). Source-mapping pages put each assumed published sentence beside its Lean transcription, so a reader can check the transcriptions without reading the proof.

Patents

US patents from my work at VMware, with co-inventors, assigned to VMware. Two themes: reinforcement-learning-based management of applications and infrastructure, including safety constraints and administrator oversight on learned controllers; and diagnosis of anomalies in distributed systems.

Full list: Google Patents search for inventor “Dev Nag”.

Writing, talks and code

Experience

  1. QueryPal (formerly CtrlStack) — Founder and CEO

    2020–present

    Led the company from cloud operations and troubleshooting to AI-powered support and enterprise workflow automation. Built production AI workflows with error correction, quality diagnostics, human review and self-hosted deployment. Work directly on the security controls, evidence and auditor coordination for annual SOC 2 examinations: Type I in 2023–2024 and Type II in 2025–2026.

  2. VMware — Office of the CTO, Cloud Management Business Unit

    2017–2020

    Founded and led Project Magna, which became vRealize AI Cloud, growing it from a seven-person team to more than 35 people across three business units. It was showcased in the VMworld 2018 executive keynote. Developed and helped launch reinforcement learning for vSAN optimization, which adapts caching and I/O configuration to changing workloads and operator-selected performance goals, with operational guardrails. The work is the basis of the patents below.

  3. Wavefront — Co-founder, CTO and CISO

    2013–2017 · acquired by VMware

    Co-founded a real-time cloud monitoring and analytics company for enterprise and SaaS engineering teams. Worked across product strategy, early enterprise sales and customer relationships. Helped raise the Series A and raised the $52 million Series B. Led the sale to VMware in 2017, reported at $375 million. As CISO, led security operations and the company's 2016 SOC 2 work.

  4. GLMX — Founder and founding engineer

    2010–2012

    Helped establish an electronic trading platform for institutional money markets, working directly with traders at JPMorgan, Bank of America, Rabobank and other institutions. GLMX has since grown into a major securities-financing platform, reporting $1.80 trillion in average daily volume in Q3 2026.

  5. PlayCafe — Co-founder and CTO

    2007–2010

    Co-founded PlayCafe, an interactive online game-show company combining live video, real-time participation and consumer software.

  6. Google — Senior Software Engineer

    2006

    Worked on the financial-processing backend supporting Google's advertising revenue.

  7. PayPal / eBay — Manager, Financial Systems Engineering

    2002–2006

    One of PayPal's first 20 engineers. Managed the Financial Systems Engineering team supporting the global payments business, defined financial-system requirements, and helped launch eBay's private-label credit line with GE Financial.

  8. Xiket — Founder and CTO

    1998–2002

    Co-founded a healthcare technology company with two Stanford physicians. Recruited and led an engineering organization of about 20, then recruited my successor as CTO.

  9. Stanford University

    B.S., Mathematics; B.A., Psychology · 1997 · then a year at the School of Medicine

    Completed the premedical curriculum alongside both degrees, and contributed to the Stanford Health Information Network for Education. Later collaborated with UCSF's Biosystems Group (2002–2006) on automated modeling and validation.

About

I work across research and engineering: choosing useful questions, building the machinery to investigate them, and making the evidence understandable to someone else.

I've founded or co-founded five companies, including Wavefront (acquired by VMware) and GLMX, and led engineering organizations from early teams to about 20 people. I hold a B.S. in mathematics and a B.A. in psychology from Stanford. I'm an angel investor in enterprise software, security and automation companies, including SecurityPal, Cortex and Magical, and I mentor startup founders.

I welcome conversations about AI assurance, evaluating self-improving systems, formal verification and circuit complexity. If you're working on a related problem, email me a short description and a link to your work.