Give AI a calculator, a proof ledger, and a CAD kernel—not another chance to guess.
Verified Technical Solver is a Codex plugin and local MCP server that moves consequential technical claims out of free-form model reasoning and into bounded, deterministic tools. It evaluates symbolic mathematics, verifies equation solutions by substitution, checks numeric relations, audits the structure of reasoning ledgers, and builds validated parametric CAD primitives with evidence artifacts.
Language models are excellent at translating intent, exploring approaches, and explaining results. They are less trustworthy when exact arithmetic, unit conversions, dependency bookkeeping, or geometric validity are left entirely to token prediction. A fluent answer can still contain a sign error, a dropped constraint, an unsupported conclusion, or an invalid solid.
This plugin gives an AI a better division of labor:
- The model handles meaning: requirements, assumptions, tradeoffs, and explanation.
- Deterministic software handles exactness: symbolic calculation, substitution, comparisons, dependency-graph checks, and CAD-kernel validation.
- The user gets evidence: exact and decimal forms, residuals, pass/fail checks, measured geometry, hashes, and explicit uncertainty.
That makes the AI better not because the plugin makes it infallible, but because it makes important claims inspectable, repeatable, and easier to falsify.
| Tool | Purpose | Evidence returned |
|---|---|---|
calculate |
Safely simplify and evaluate bounded mathematical expressions | Exact value, decimal value, LaTeX, free symbols |
solve_equations |
Solve bounded symbolic equation systems | Solutions, substitution residuals, verified flag |
verify_relations |
Check equality, approximation, and inequalities | Per-check difference and pass/fail result |
audit_reasoning_structure |
Find missing support, broken references, duplicate IDs, and dependency cycles | Structured issue report and conclusion coverage |
build_box_part |
Create plates/boxes with fillets and through-holes | Kernel validity, solid count, dimensions, volume, area, STEP/STL/SVG, SHA-256 |
build_cylinder_part |
Create cylinders and tubes | Kernel validity, measured geometry, exports, verification report |
- It never uses Python
eval; expressions are parsed through a small AST allowlist. - Inputs have bounds for expression size, syntax nodes, symbols, equations, solutions, dimensions, holes, and worker output.
- Each operation runs in a subprocess with a timeout, isolating failures from the MCP server.
- Equation solutions are checked by substitution.
- CAD output must be one kernel-valid solid and is measured after construction.
- Output paths are restricted to
VTS_OUTPUT_ROOTand existing artifacts are never overwritten. - Reasoning audits are described honestly: they validate structure, not whether natural-language premises are true.
- Python 3.11+
- Codex with plugin/MCP support
- Dependencies in
requirements.txt(mcp,sympy, andcadquery)
git clone https://github.com/ASVLCII/verified-technical-solver.git
cd verified-technical-solver
python -m venv .venvActivate the virtual environment, then install dependencies:
python -m pip install -r requirements.txtThe included .mcp.json starts scripts/server.py with python. If Codex does not launch inside your activated environment, replace command with the absolute path to the virtual environment's Python executable.
Optionally set VTS_OUTPUT_ROOT to control where CAD artifacts may be written. Without it, output is restricted to ~/Documents/Codex.
Use Verified Technical Solver to solve x + y = 5 and x - y = 1. Verify every solution by substitution.
Check whether this tolerance stack remains below 0.25 mm. State assumptions and show each deterministic relation check.
Create a 60 mm × 30 mm × 4 mm plate with four 4 mm through-holes and a 2 mm edge fillet. Export STEP, STL, and a dimensioned SVG, then report kernel validity and hashes.
Build a reasoning ledger for this engineering recommendation, audit its structure, and distinguish evidence from assumptions and judgment.
- Restate the objective, known values, units, constraints, and missing engineering inputs.
- Separate semantic judgment from mechanically verifiable claims.
- Route quantitative dependencies through deterministic tools.
- For difficult problems, compare materially different approaches.
- Record conclusions in a reasoning ledger with stable IDs, dependencies, evidence, and explicit assumptions.
- Audit the ledger, then independently inspect semantic validity.
- Use substitution, dimensional analysis, boundary cases, or another independent route for consequential results.
- Report failures and uncertainty alongside successful checks.
See verification-protocol.md for the evidence classes and CAD acceptance criteria.
python scripts/test_solver.py
python scripts/test_mcp.pyThe tests cover exact calculation, substitution, rejected code execution, bounded factorials, visible relation failures, reasoning cycles, CAD dimensions and volume, invalid/overlapping geometry, output confinement, overwrite refusal, MCP initialization, and recovery after a rejected call.
- The reasoning audit checks graph structure and evidence bookkeeping; it is not a theorem prover or truth oracle.
- CAD generation currently supports exact box/plate and cylinder/tube primitives, not arbitrary assemblies or free-form surfaces.
- A kernel-valid model is not automatically manufacturable. Tolerances, fits, material, loads, process constraints, and regulatory requirements still need qualified engineering judgment.
- Symbolic computation can be expensive; the server applies bounds and timeouts, but it is not intended for untrusted public multi-tenant execution.
.codex-plugin/plugin.json Plugin metadata
.mcp.json Local MCP server declaration
scripts/server.py MCP interface and worker isolation
scripts/worker.py Math, reasoning, and CAD implementation
scripts/test_solver.py Deterministic unit tests
scripts/test_mcp.py MCP integration test
skills/verified-technical-solver/ Agent workflow and verification protocol
Contributions are welcome—especially new independently verifiable operations, stronger resource bounds, additional geometry acceptance tests, and cross-platform installation improvements. Read CONTRIBUTING.md before opening a pull request. Please report security issues privately as described in SECURITY.md.
MIT © ASVLCII. See LICENSE.