ShadowProof Bridge is a self-hostable paraconsistent HoTT LLM-to-Lean acceptance gateway.
It accepts Lean 4 proof attempts or structured proof proposals produced by an LLM, runs them through security preflight, theorem-fingerprint locking, and Lean validation, then routes the result through a 4-valued ShadowHoTT bilattice state machine.
v25.8 adds audit-enhanced evaluation metrics, proof-lifecycle observability, bilattice routing counters, human-review escalation metrics, and retrieval metadata hooks for theorem dependency and structure-aware indexing.
ShadowProof is designed for proof-assistant workflows where ordinary pass/fail validation is too coarse. Failed proof attempts may still contain useful repair structure. Accepted Lean code may still conflict with external refutation signals. Repair loops need stable mathematical governance rather than untracked retry logic.
ShadowProof provides that governance layer.
ShadowProof Bridge sits between:
- LLM-generated mathematical reasoning
- Lean/Mathlib validation
- Human or automated proof-repair workflows
- Audit and observability systems
It is not a general chatbot and not a replacement for the Lean kernel.
Its role is to govern proof attempts before, during, and after Lean validation by tracking:
- proof acceptance,
- repairable failure,
- rejection,
- unchecked states,
- contradiction-bearing states requiring human review,
- theorem-target drift,
- security preflight failures,
- proof fingerprint preservation,
- repair-loop behavior,
- bilattice routing decisions,
- and proof-lifecycle metrics.
At a high level, ShadowProof Bridge:
- Accepts a direct Lean 4 proof attempt or structured
DraftProposal. - Runs security preflight checks.
- Locks the intended theorem fingerprint.
- Checks or delegates Lean validation.
- Computes a ShadowHoTT bilattice state.
- Routes the attempt to one of the supported dispositions:
accept
repair
reject
human_review
unchecked
- Emits evaluation and observability metadata for pilot analysis.
This allows the system to preserve useful failed proof structure without pretending that all failed attempts are worthless, while also preventing contradiction-bearing states from being silently auto-accepted.
The runtime uses a finite four-valued bilattice:
[ L = \mathrm{Bool} \times \mathrm{Bool} ]
with coordinates:
[ (t, r) = (\text{truth signal}, \text{refutation signal}) ]
The four canonical values are:
top = (true, false)
bottom = (false, true)
both = (true, true)
neither = (false, false)
Designation is the predicate:
[ t = \mathrm{True} ]
Designation is not a probability, not a confidence score, and not a neural heuristic.
Path composition is modeled by the bilattice meet:
(t_1 \wedge t_2,; r_1 \vee r_2) ]
Truth is fragile. Refutation accumulates.
The De Morgan involution is coordinate swap:
[ (t, r) \mapsto (r, t) ]
It has order two, fixes both and neither, swaps top and bottom, and is deliberately not designation-preserving.
Lean-accepted states with a simultaneous refutation signal are designated but not auto-accepted. They route to:
human_review
This is the central ShadowHoTT safety rule: contradiction-bearing acceptance is visible, typed, measured, and routed. It is not hidden inside an ordinary success state.
ShadowProof includes a Lean-side reference model of its finite ShadowHoTT governance semantics.
The Lean governance core formalizes:
- the four-valued Shadow bilattice;
- truth and refutation coordinates;
- designation;
- bilattice meet and join;
- De Morgan coordinate swap;
- disposition routing;
- theorem-fingerprint preservation;
- patch morphism structure;
- and the No-Glutty-J safety invariant.
The production Python runtime remains the operational gateway. The Lean model is the kernel-checked semantic mirror used to prevent mathematical drift in the routing layer.
This is not a replacement for the Lean kernel and not a full HoTT implementation. It is a finite, auditable, HoTT-inspired governance layer for contradiction-aware proof validation and repair.
Ordinary proof pipelines often collapse proof attempts into a binary outcome:
pass / fail
ShadowProof instead separates truth and refutation signals.
This makes the following distinctions explicit:
| State | Meaning | Routing |
|---|---|---|
| Truth without refutation | accepted proof signal | accept |
| Refutation without truth | failed or rejected proof signal | reject or repair |
| Neither truth nor refutation | unchecked or unavailable validation | unchecked |
| Truth and refutation together | accepted but contradiction-bearing | human_review |
The purpose is not to weaken Lean. Lean remains the kernel authority.
The purpose is to prevent proof-repair systems from losing information when reasoning, tests, formal validation, and external contradiction signals conflict.
v25.8 adds practical, pilot-safe improvements from the audit roadmap without overclaiming unfinished enterprise features.
New or expanded capabilities include:
- richer evaluation metrics;
- human-review escalation accuracy;
- token-count metrics;
- p95 latency reporting;
- drift-escape-rate tracking;
- proof-lifecycle trace helpers;
- bilattice decision counters;
- human-review routing counters;
- retrieval dependency metadata;
- structure hashes for theorem/proof retrieval;
- LSH-style retrieval buckets;
- optional dependency graph sidecar support.
These features improve diligence, pilot analysis, and future optimization without changing the finite ShadowHoTT core semantics.
ShadowProof Bridge v25.8 includes:
- dependency-light ASGI app:
shadowproof_core.asgi:app - stdlib HTTP server:
shadowproof serve - per-connection timeout on the stdlib HTTP server
- bearer-token local pilot mode
- OIDC/JWT authentication scaffold
- optional Postgres storage backend
- optional Redis quota backend
- active readiness checks
- Prometheus metrics
- structured JSON access logs
- OpenTelemetry span hooks
- proof-lifecycle trace helpers
- bilattice routing counters
- human-review escalation metrics
- OpenAPI 3.1 schema generation
- deliberately minimal TypeScript MCP bridge
- Docker Compose pilot stack under
deploy/ - API service container
- Lean-worker stub container
- Postgres container
- Redis container
- Prometheus container
- in-process ShadowHoTT bilattice reports
- runtime De Morgan symmetry report
- offline training-capacity planner
- ShadowHoTT eval command
- regression-suite command
- audit-enhanced eval harness
- retrieval metadata hooks
- buyer-demo script
- acquisition/diligence documentation under
docs/acquisition/ - security documentation in
SECURITY.md - local smoke tests and regression tests
The package is structured for private diligence review, controlled pilots, and integration into a real Lean/Mathlib validation environment.
This repository is an acquisition-clean pilot artifact, not a finished enterprise SaaS product.
The following are intentionally not bundled:
The shipped LLMBridgeTranslator is a deterministic scaffold.
It recognizes a small number of hardcoded English theorem families:
- group associativity,
- group left-cancellation,
- group commutativity as a deliberate drift trap.
Unsupported requests route to unsupported.
The package does not pretend to translate arbitrary mathematics from English into Lean.
The frontier-model path is exposed through shadowproof_model_provider_call, which posts a generic JSON envelope only to server-configured provider URLs.
Caller-supplied provider URLs, caller-supplied headers, and caller-supplied bearer tokens are rejected.
Specific adapters for frontier providers are not bundled.
Production deployments must run the Lean worker inside an isolated environment such as:
- Docker,
- gVisor,
- Firecracker,
- Kubernetes with strict resource controls,
- or an equivalent hardened execution boundary.
The Python package itself does not provide a kernel sandbox.
The audits that produced the v0.25.2, v0.25.3, v0.25.4, v0.25.6, v0.25.7, and v0.25.8 hardening patches were internal exercises.
Third-party security review remains outstanding for enterprise general availability.
The shipped examples and evals are smoke-test sized.
Real deployment requires larger customer-specific corpora.
The framework includes training-capacity planning, policy scaffolding, and audit metrics, but a trained production policy must be populated from real customer evals.
v25.8 adds retrieval metadata hooks, dependency graph sidecar support, structure hashes, and LSH-style buckets.
It does not bundle a full production Mathlib GraphRAG system, dense embedding service, vector database, or theorem-dependency pipeline at Mathlib scale.
Representative layout:
shadowproof_core/
asgi.py
cli.py
eval_harness.py
lean_lex.py
observability.py
repair.py
retrieval.py
security.py
tool_api.py
...
lean_project_template/
ShadowProof/
BilatticeCore.lean
Routing.lean
PatchMorphism.lean
NoGluttyJ.lean
DemorganSymmetry.lean
deploy/
docker-compose.yml
lean-worker.Dockerfile
...
docs/
acquisition/
DILIGENCE_INDEX.md
DILIGENCE_STATUS.md
CLAIMS_BOUNDARY.md
EVAL_OBSERVABILITY_RETRIEVAL_V25_8.md
SHADOWHOTT_LEAN_GOVERNANCE.md
...
examples/
evals/
optimization/
tool_requests/
mcp/
src/
dist/
package.json
schemas/
openai_mcp_tool_descriptors.json
shadowproof_index_mathlib.input.schema.json
scripts/
run_buyer_demo.sh
ci_secret_scan.py
tests/
test_v25_7_shadowhott_governance.py
test_v25_8_audit_ideas.py
...
Primary diligence documents live in:
docs/acquisition/
Start with:
docs/acquisition/DILIGENCE_INDEX.md
docs/acquisition/DILIGENCE_STATUS.md
docs/acquisition/CLAIMS_BOUNDARY.md
SECURITY.md
CHANGELOG.md
PATCH_NOTES_V25_8.md
From the repository root:
pip install -e .For production/pilot extras:
pip install -e '.[prod]'Run the Python test suite:
python -m pytest tests/ -qRun the De Morgan symmetry report:
python -m shadowproof_core.cli demorgan-symmetry examples/tool_requests/demorgan_symmetry.jsonRun the offline training-capacity planner:
python -m shadowproof_core.cli training-capacity-plan examples/optimization/training_capacity_plan.jsonRun the ShadowHoTT eval:
python -m shadowproof_core.cli shadowhott-eval examples/evals/shadowhott_eval.jsonRun the regression suite:
python -m shadowproof_core.cli regression examples/evals/regression_suite.jsonRun the secret scan:
python scripts/ci_secret_scan.pySet local bearer-token auth:
export SHADOWPROOF_AUTH_MODE=bearer
export SHADOWPROOF_BEARER_TOKENS=dev-token:defaultStart the stdlib server:
python -m shadowproof_core.cli serve --host 127.0.0.1 --port 8765In another shell:
curl -sS -X POST http://127.0.0.1:8765/shadowproof_shadowhott_state \
-H 'Authorization: Bearer dev-token' \
-H 'Content-Type: application/json' \
-d '{"request_id":"smoke","proof_graph":[],"lean_status":"not_run","status":"unchecked"}'Install production extras:
pip install -e '.[prod]'Run with Uvicorn:
uvicorn shadowproof_core.asgi:app --host 0.0.0.0 --port 8765From the deployment directory:
cd deploy
docker compose up --buildImportant note:
The bundled Lean-worker container is a stub. Replace:
deploy/lean-worker.Dockerfile
with a real Lean 4 / Mathlib image before running the validation path in a serious pilot.
Against the stub, the bridge should report:
lean_status: not_available
That is expected behavior.
Run:
bash scripts/run_buyer_demo.shThe buyer demo walks through:
- bilattice axiom report,
- offline capacity plan,
- ShadowHoTT eval,
- regression suite,
- commercial-section endpoints.
It exits 0 and prints JSON for every section when the local environment is configured correctly.
The repository includes a deliberately minimal TypeScript MCP bridge under:
mcp/
Build it with:
cd mcp
npm ci --ignore-scripts
npm run buildThe MCP bridge is intentionally narrow. It is present for integration demonstration and OpenAI-native tool-surface compatibility, not as a full SDK.
The in-process tool registry contains 84 tools.
Of these, 35 are declared in:
schemas/openai_mcp_tool_descriptors.json
The omitted tools are admin, domain-pack, and promotion tools that are not part of the buyer-facing API surface.
All HTTP/ASGI tool routes resolve to input schemas.
High-risk routes use strict exact schemas where possible.
v25.8 expands the evaluation and observability layer.
The eval harness can now report metrics such as:
- total cases;
- accepted cases;
- rejected cases;
- repair cases;
- unchecked cases;
- human-review cases;
- human-review escalation accuracy;
- drift escape rate;
- token totals;
- token averages;
- latency averages;
- p95 latency.
The observability helpers expose proof-lifecycle and bilattice decision metadata suitable for structured logs, OpenTelemetry spans, or downstream pilot dashboards.
This gives pilot deployments a clearer way to measure whether repair routing is improving, whether drift escapes are decreasing, and whether contradiction-bearing states are being escalated correctly.
v25.8 adds retrieval metadata hooks for future Mathlib/domain-pack indexing.
The retrieval layer can attach:
- theorem dependency metadata;
- structure hashes;
- LSH-style buckets;
- optional dependency graph sidecar information.
This is not a full dense-vector theorem retriever. It is a safer intermediate layer that prepares the project for hybrid retrieval and GraphRAG without creating false production claims.
See:
SECURITY.md
for the full threat model and hardening notes.
Security hardening applied across v0.25.2, v0.25.3, v0.25.4, v0.25.6, v0.25.7, and v0.25.8 includes:
- server configuration comes from environment variables only;
- request bodies cannot override server configuration;
- tenant identity is bound to the authenticating credential;
- payload-supplied
tenant_idmust match the authenticated tenant; - tenant directory paths reject
..,., and dots-only ids; relative_to()is enforced as defense in depth;- rejection memory is tenant-scoped by default;
- stdlib HTTP server has a per-connection timeout;
- quota mode comparisons are normalized before rate-limit checks;
- Memory/Redis quota modes cannot bypass enforcement through casing drift;
- all HTTP/ASGI routes resolve to input schemas;
- high-risk routes use strict exact schemas where possible;
- additional file-reading and file-writing paths are root-guarded;
- domain-pack list/get/retrieval share the same allowed-root policy;
- file-writing HTTP routes are admin-scoped;
- Lean comment and literal masking is delimiter-aware;
- nested Lean block comments are handled;
- proof-body repair replacement uses a delimiter-aware anchor splitter rather than raw regex substitution;
- audit metrics distinguish human-review escalation from ordinary acceptance.
v25.6 hardened Lean parsing-adjacent code.
Key changes included:
- Lean comment and string masking became delimiter-aware.
- Nested Lean block comments became handled.
- Lean comment markers inside string literals no longer hide real declarations.
- Security preflight, theorem-lock, and ShadowHoTT fingerprint obstruction checks share the safer masking behavior.
- Proof-body repair replacement no longer depends on fragile raw regex substitution.
- Replacement now uses a delimiter-aware anchor splitter.
v25.7 added the Lean-formalized ShadowHoTT governance core.
v25.8 added audit-enhanced evaluation, observability, and retrieval metadata hooks.
A standalone Lean 4 / Mathlib formalization of the De Morgan symmetry and bilattice governance claims is included under:
lean_project_template/ShadowProof/
Relevant files include:
BilatticeCore.lean
Routing.lean
PatchMorphism.lean
NoGluttyJ.lean
DemorganSymmetry.lean
The runtime counterparts are:
shadowproof demorgan-symmetry
bilattice_axiom_report()
The intended relationship is:
- Lean file: formal reference template.
- Runtime report: in-process operational counterpart.
- Tests: regression guard against semantic drift.
Production diligence should include a fresh Lean/Mathlib transcript generated in the buyer’s target Lean environment.
The ShadowHoTT finite bilattice layer is intentionally small and explicit.
The package claims:
L = Bool × Bool;- designation is
truth == True; - De Morgan duality is coordinate swap;
- the swap has order two;
- the swap fixes
bothandneither; - the swap exchanges
topandbottom; - the swap is not designation-preserving;
- path composition is
(t₁ ∧ t₂, r₁ ∨ r₂); - Lean-accepted plus refuted states route to
human_review; - patch morphisms must preserve theorem fingerprints;
- No-Glutty-J monitoring prevents contradiction-bearing states from being silently auto-accepted.
The package does not claim that the finite bilattice itself proves arbitrary mathematics.
It governs proof-attempt disposition around Lean validation.
ShadowProof Bridge v25.8 is:
pilot-ready
buyer-demo-ready
private-diligence-ready
audit-enhanced
acquisition-clean
It is not yet:
enterprise-GA
externally security-certified
production-SLA-backed
fully provider-adapter-complete
trained on real customer corpora
production-Lean-worker-complete
full-Mathlib-GraphRAG-complete
This distinction is intentional.
The repository is suitable for technical diligence, controlled pilots, and acquisition evaluation.
Before enterprise general availability, the following remain outstanding:
- External security review by a third-party firm.
- Legal and SLA work.
- Signed certificate / registry publishing pipeline.
- Large customer evaluation corpora.
- Real Lean CI transcript at production scale.
- Customer-specific frontier-model adapters.
- Customer-specific retrieval integrations.
- Production isolated Lean worker.
- Trained policy file populated from real customer evals.
- Deployment-specific observability and incident-response procedures.
- Production Mathlib dependency extraction and retrieval pipeline.
- Container signing and supply-chain provenance.
ShadowProof Bridge is best understood as:
A paraconsistent HoTT bridge between LLM proof generation and Lean validation,
with bilattice-governed repair, rejection, acceptance, human-review routing,
and audit-ready proof lifecycle observability.
A longer description:
ShadowProof Bridge is a self-hostable paraconsistent HoTT LLM-to-Lean gateway
for contradiction-aware proof validation and repair. It routes Lean proof attempts
and LLM-generated proof proposals through security preflight, theorem-fingerprint
locking, Lean validation, and 4-valued ShadowHoTT bilattice semantics, preserving
useful repair structure while preventing contradiction-bearing states from being
silently auto-accepted. v25.8 adds audit-enhanced metrics, proof-lifecycle
observability, and retrieval metadata hooks for controlled pilots and diligence.
This is a private acquisition/diligence repository.
Do not treat this repository as a public production SaaS release unless and until the outstanding GA items have been completed.
For diligence review, begin with:
docs/acquisition/DILIGENCE_INDEX.md
docs/acquisition/DILIGENCE_STATUS.md
docs/acquisition/CLAIMS_BOUNDARY.md
docs/EVAL_OBSERVABILITY_RETRIEVAL_V25_8.md
docs/SHADOWHOTT_LEAN_GOVERNANCE.md
SECURITY.md
CHANGELOG.md
PATCH_NOTES_V25_8.md