EqTrace

Inspectable contracts between papers, code, and execution.

Interactive demo · Technical report (PDF) · LaTeX source · 中文说明 · Evidence boundaries

EqTrace connects LaTeX equations and pseudocode to executable code, then places those local contracts inside a project graph of datasets, multi-file blocks, virtual interfaces, and recorded runs. It helps review whether a change still implements the described method.

Try the complete example

Requires Python 3.11+ and uv. From a clone of this repository:

make setup             # locked environment; Z3, NumPy demo, tests, browser tools
make test              # parser, proof, runtime, freshness, and interface checks
make demo              # actual checks and pipeline execution; export both workbenches

Open artifacts/engineering/index.html for the 36-file / 2-codebase engineering example. Open artifacts/equations/index.html for formula/code comparison. These HTML files are self-contained and work offline. Committed snapshots are in docs/demo; regenerate them before claiming freshness on another environment.

The source graph starts with a package overview. Select a package and Open files to see its files and direct dependencies; Focus direct connections isolates a local neighborhood. Both engineering graphs use dependency layers and support direction changes, zoom, drag-to-pan, and SVG export.

For live formula editing, run make serve, then open the local workbench. Changing the implementation exposes changed operations, counterexamples, and failing execution samples. The browser service only checks temporary scalar source pairs.

What connects to what?

flowchart TD
    P[LaTeX equations or pseudocode] --> IR[Ordered scalar representation]
    C[Independent Python functions] --> IR
    IR --> V[Structure + real equivalence + sampled execution]
    R[Multiple codebase roots] --> S[Static symbols and candidate dependencies]
    D[CSV / JSONL datasets] --> T[Observed schema and generated LaTeX table]
    M[Declared blocks and virtual interfaces] --> G[Hierarchical engineering graph]
    S --> G
    T --> G
    X[Explicit pipeline run] --> E[Observed calls / array shapes / output writes]
    E --> G
    V --> G
    G --> W[Interactive flows and machine-readable evidence]

Loading

The graph keeps these claims separate:

Evidence	What it supports
Declared block meaning / ports	The author's intended semantics and dataflow
Static observations	Current files, symbols, imports, and candidate calls
Recorded execution	Selected main-thread calls, array shapes, output-write events, and hashes
PROVED_REAL scalar leaf	Conditional real equivalence under the accepted translation and domain
Successful sampled comparison	Agreement on the actual executed scalar samples

A block can contain many files across codebases, have a parent, and appear in several named flows. A virtual entity can be an in-memory tensor, checkpoint, prepared dataset, or metric record. Its shape contract binds to an explicit function argument or return value. Engineering guide →

A small equation contract

A paper equation and implementation remain independent sources:

\begin{equation}\label{eq:loss}
 e = (a-b)^2
\end{equation}

def squared_error(a, b):
    difference = a - b
    return difference * difference

Bind them with a manifest:

schema_version = 1
paper_sources = ["method.tex"]

[[contracts]]
id = "loss"
label = "eq:loss"
implementation = "loss.py"
function = "squared_error"
inputs = ["a", "b"]
domains = {a = [-10, 10], b = [-10, 10]}
policy = "algebraic"

Run code/.venv/bin/eqtrace check eqtrace.toml. A strict pass requires a resolved binding, accepted domain, real-equivalence result, and successful current-source execution. ordered policy also requires the same ordered computation. Removing an epsilon, introducing an unmodeled fallback, or leaving a stub prevents a strict pass.

Translation in both directions

code/.venv/bin/eqtrace translate examples/formula.txt --from latex --inputs x,mu,sigma,epsilon
code/.venv/bin/eqtrace translate examples/implementation.py --from python --function normalize

Each exports minimal Python, LaTeX, algorithmic pseudocode, text pseudocode, graph JSON, Mermaid, and SVG. LaTeX pseudocode uses --from pseudocode and an explicit input list. Translation alone is labeled unexecuted and unproved. Supported syntax and failure states are documented in the equation guide.

Check a real engineering run

code/.venv/bin/eqtrace trace examples/engineering/architecture.toml sequence-run
code/.venv/bin/eqtrace architecture examples/engineering/architecture.toml \
  --require-runs --out artifacts/engineering

The example reads 384 synthetic records, prepares arrays, runs a frozen attention encoder, trains and fine-tunes a regression head, and exports checkpoints, predictions, and metrics. Only the head is optimized. Four declared NumPy interface shapes are checked against real calls. One proven squared-error leaf is called by the prediction writer. Example manifest →

The trace command executes the declared project entry point with ordinary user permissions. Use it with trusted code. architecture scans and audits existing evidence; it does not execute the pipeline.

Validate the tool against its own paper

selfcheck.toml binds two formulas and one algorithm in the report to the actual discrepancy kernels used by EqTrace. The root architecture.toml scans the checker itself and attaches these contracts to its checker block. This is self-application with a circular trust boundary, not verification of the checker.

The released synthetic corpus contains 18 authored cases: 4 valid and 14 invalid or unsupported. All expected classifications matched; a midpoint-only comparison accepted 4 invalid cases. These are regression results, not independent benchmark estimates. Retained evidence →

Development and paper

make test
make demo
make build
make paper             # XeLaTeX + latexmk + biber + documented fonts/packages
# In another terminal, with make serve running:
code/.venv/bin/python -m playwright install chromium
make browser

See build and contribution instructions, architecture, and reference provenance. The Python core has no runtime dependencies. Z3 is an explicit proof extra; NumPy is used by the engineering demo. No external AI service, Lean installation, API key, or private dataset is required.

Current proof boundary: scalar arithmetic in a fully consumed restricted grammar. Whole pipelines, arbitrary tensor kernels, scientific meaning, all-input floating-point behavior, and the checker itself are not proved. Unknown solver outcomes and unsupported constructs cannot become strict passes. General Python can still be inspected at the static/trace layer. Trust model →

MIT licensed. Please cite the software when using EqTrace in research; the accompanying report documents the method. Inspired by Prove2Me, I Heart LA / HeartDown, and computation-linked visual inspection. EqTrace currently produces Z3 evidence, not Lean proof certificates.

Citation and contact

EqTrace is a personal side project by Shiqi Wang. Contact: qtec@outlook.com.

Wang, S. (2026). EqTrace: Inspectable Contracts between Papers, Code, and Execution (Version 0.1.0) [Computer software]. GitHub. https://github.com/Mappedinfo/eqtrace/releases/tag/v0.1.0

Use GitHub's Cite this repository panel for APA and BibTeX, or download CITATION.bib. A DOI has not yet been registered. Citation and Zenodo archiving instructions explain the next step and the difference between version and concept DOIs.