FormulaTracer

English | 日本語

From scientific code to auditable mathematics.

FormulaTracer is an experimental, fail-closed semantic auditor for scientific software. It reconstructs mathematical meaning from code, then keeps exact and non-exact relations, assumptions, proof obligations, numerical evidence, provider contracts, provenance, and source localization in one structured workflow. A separately declared theory is optional.

When FormulaTracer cannot justify an interpretation, it reports UNRESOLVED instead of guessing. Structural similarity is not proof, numerical similarity is not a certified bound, and provider retrieval is not verification.

Public references: Python functions · Rust · C ABI · C++ · result/status/evidence · providers · physics · user-defined semantics

Why FormulaTracer?

A formula alone does not say whether the implementation is exact or approximate, which assumptions it needs, where it came from, or which source span caused a divergence. FormulaTracer connects those questions through one Rust-owned semantic model and returns a structured VerificationResult or ReconstructionResult; TeX, JSON, and explanations are derived views.

Typical uses include scientific implementation review, model-change review, pre-publication checks, reproducibility work, and inherited-code assessment.

Install

Python 3.10 or newer is required. Published supported wheels are intended to include the native core, so end users do not need Rust, Cargo, or CMake.

python -m pip install formulatracer

This repository is currently version 0.1.0; package publication is not part of this readiness work. Source developers need Rust 1.85+, and the optional C++ frontend requires LLVM/Clang major 18 and a C++20 build toolchain.

Quick start: audit code without a theory

Clone the repository, install it, then run the synthetic example:

python -m pip install -e .
formulatracer python-audit examples/python_audit/weighted_sum.py --function calculate_weighted_score --output weighted_score --mode REPORT_ONLY --report output/python-audit/report.md --json-output output/python-audit/audit.json --no-lean

The report contains the independently reconstructed implementation expression, numeric backward slice, assumptions, provider contracts, provenance, and any unresolved boundary. No theory annotation is required.

An optional stronger comparison can be added when a theory is available:

from formulatracer import FormulaTracer

formula = FormulaTracer.from_tex(r"\sum_{i=0}^{N-1} x_i")
plan = formula.plan_generation(language="python", search="broad")
print(plan.explain(limit=5))
generated = formula.generate(language="python", auto_select=True)
result = generated.verify()
print(result.status)
print(result.independent_audit)

Candidate similarity only starts an investigation. Selection still requires typed unification, constraints, authorized transformations, and independent re-analysis.

Core workflow

Scientific source -> Implementation IR -> Mathematical reconstruction
  -> Exact/relational analysis -> Assumptions and obligations
  -> Error/range and provider evidence -> Provenance and localization
  -> Structured result -> AuditBundle / TeX / JSON / explanation

Main Python entry points are FormulaTracer.from_source, FormulaTracer.analyze, FormulaTracer.from_tex, plan_generation, reconstruct, and the native structured-result wrappers. See the Python API instead of relying on internal cpp_audit modules.

Supported languages

The FormulaTracer C++ components build as C++20. The native CLI currently operates on semantic documents (canonicalize, tex, compare); it is not a complete Rust-source audit CLI. See language support.

Scientific libraries and providers

Provider contracts cover selected public APIs, not an entire upstream library. Most external library entries are currently REFERENCE_ONLY_VERSION_UNPINNED; therefore this release does not promise a broad NumPy/SciPy/xarray version range. Axis, dtype, missing-value, named- dimension, device, laziness, mutation, and default semantics remain explicit contract conditions. See the provider matrix.

User-defined semantics: a redundant evidence path

@cpp_audit.theory(output=..., expression=...) supplies a user declaration to the same Mathematical IR, relation, evidence, and provenance pipeline used by automatic reconstruction. It is useful for private callbacks, future libraries, hardware kernels, and source that is unavailable to the auditor. It is not a second evaluator and a declaration alone never becomes implementation-, reference-, or Lean-verified evidence.

When implementation-derived mathematics is available, FormulaTracer reports MATCH, MISMATCH, or NOT_EVALUABLE between the two independent paths. Callback value semantics and effects are separate: an expression may be retained while purity remains UNKNOWN_EFFECT. See user-defined semantics.

Physics foundation

The versioned physics foundation defines multivariable/vector calculus, geometric integral relations, dimensions and frames, SO(3)/quaternion representations, Fourier/Laplace relations, numerical realizations, and selected SciPy callback boundaries. Support levels are reported separately as DEFINED, THEOREM_REGISTERED, LEAN_KERNEL_VERIFIED, REALIZATION_AVAILABLE, CONDITIONAL, or PARTIAL.

FormulaTracer audits mathematical and implementation relations. It does not prove that a physical law is empirically true. General Noether, Gauss/Stokes, SE(3), finite-volume error, and AD claims remain conditional unless their listed obligations are discharged. See the physics support boundary.

Platform status

Evidence model

• KERNEL_VERIFIED: checked by the Lean kernel.
• KERNEL_VERIFIED_UNDER_ASSUMPTIONS: kernel-checked with listed assumptions.
• FORMALLY_DERIVED: derived from versioned rules and evidence.
• REFERENCE_CONTRACT: backed by an upstream public reference.
• EMPIRICALLY_VALIDATED / RUNTIME_EVIDENCE: tests or a concrete run, not proof.
• UNRESOLVED: ambiguity, unsupported behavior, missing contract, or open obligation.

Exact equality, approximation, discretization, truncation, sampling, and algorithmic realization are distinct relations. Read proof levels and the trust boundary.

Examples

• Theory-free Python audit
• Exact, non-exact, and unresolved operational audit
• Rust-only consumer
• C-only consumer
• C++ RAII consumer

Non-goals and limitations

FormulaTracer does not prove compilers, CPUs, every external implementation, or a researcher's scientific intent, and is not a general compiler, numerical solver, CAS, Lean replacement, or arbitrary-software verifier. It does not silently infer unknown semantics and does not replace scientific judgement. Complete Rust-source native audit orchestration is not yet exposed by formulatracer-native. Performance is secondary to semantic correctness and fail-closed behavior.

Runtime-only call targets, non-exhaustive dynamic keys, unknown backends, impure/opaque callbacks, and unproved conditional theorems remain partial or unresolved. “Currently unresolved” does not mean “fundamentally impossible”; user contracts, runtime evidence, or provider evidence may close some cases, but those evidence classes are never relabelled as static proof.

Documentation and support

Start with the class and function usage guide (日本語) or the documentation index. Use GitHub Issues for bugs and GitHub Discussions for usage questions. Report vulnerabilities privately as described in SECURITY.md.

Citation, license, and contributing

Citation metadata is in CITATION.cff. FormulaTracer is licensed under Apache-2.0; third-party categories and redistribution notes are in THIRD_PARTY_NOTICES.md. Generated-code licensing depends on user input, selected templates, and upstream provenance; generation does not automatically impose the FormulaTracer project license on all output.

Contributions should preserve fail-closed behavior, add positive/negative/ unresolved tests, and record non-blocking findings in the defect ledger. See CONTRIBUTING.md.