VVUQ4AI

VVUQ4AI (verification, validation and uncertainty quantification for AI) checks the mathematics and code that AI agents produce for science and engineering. An agent sends a claim, the service runs a real tool on it, and the answer comes back with the artifact that produced it, so the claim can be checked rather than trusted.

What runs today:

• Lean 4: proofs are compiled with the Lean 4 toolchain and matched against the stated theorem.
• SymPy: symbolic identities are checked by computer algebra.
• Z3: constraint and satisfiability questions are solved by an SMT solver.
• Loogle: Mathlib is searchable by type signature.
• Rulesets: designs are checked rule by rule against engineering standards such as IEEE 802.3.
• Knowledge search: a graph of physics, mathematics and engineering results is searchable by meaning.

The same core is served as an HTTP API and as an MCP server for agents. Open bounties reward Lean proofs that the service accepts.