FormulaTracer v0.1.0
FormulaTracer v0.1.0
FormulaTracer v0.1.0 is the first public release from the sanitized, independent public history.
Highlights
- Fail-closed mathematical reconstruction and verification for scientific Python, C++, and Rust workflows.
- Rust semantic core with Stable C ABI v1 and Python/C++ facades.
- Structured verification results with TeX/JSON rendering, provenance, error/range evidence, and debugger information.
- Lean 4.19.0 proof-layer integration.
- Public API documentation in English and Japanese.
Validation
Release commit: 6edf24d59ea2f2a29ca33db1794cb5137b1f2117
- Tier 1 compatibility checks passed for Python 3.10–3.13 and Rust 1.85/stable.
- Tier 2 semantic integration, native consumers, Clang 18, Lean, native differential, and structural-isomorphism checks passed.
- Windows and Linux package jobs passed.
- The attached Windows wheel was clean-installed and its native library loaded successfully.
- The attached Linux wheel was clean-installed on the recorded Ubuntu 24.04/glibc 2.39 runner.
- The attached sdist was source-built and clean-installed successfully.
- Artifact privacy scans reported zero private-path hits and no protected DOCX.
The Tier 3 workflow's final clean-tree check reported only a recorded reference-access date changing from 2026-08-29 to 2026-08-30. All preceding semantic, proof, provider, packaging, and platform steps passed. This non-semantic exception is recorded in artifact-manifest.json.
Supported release artifacts
- Windows x86_64 wheel
- Linux x86_64 wheel
- Source distribution
- SPDX SBOM
- Artifact/provenance manifest
- SHA-256 checksums
Important boundaries
- Provider contracts cover selected documented APIs; they are not a claim of complete support for every upstream library or version.
- The Linux wheel is validated for the recorded runner environment and is not a universal all-distributions compatibility claim.
- The C++ frontend requires LLVM/Clang major 18.
- macOS wheels are not included.
- Runtime agreement is evidence, not automatically a formal proof. Evidence levels and unresolved assumptions remain explicit.
The previous private repository history and private v0.1.0 release remain unchanged. This public repository uses an independent sanitized history.