Prove the Python backend through proven Rust.
A Python project is designed to go through the same pipeline with one extra front end: pure, fully type-hinted spans will be ported to Rust in the provable subset, called from the patched Python through a compiled extension, and proven. By design, the proven Rust runs only inside the approved precondition; outside it, the original Python runs unchanged.
Find, port, guard, prove.
From the port onward it will be the Rust pipeline: extract, spec, prove, check. The port is designed to be validated like a patch: by differential tests and by the person reading the diff.
A FastAPI billing handler.
Spec.prorateIllustrativeFor integer amounts and periods that fit in 64 bits, where the period is at least one day, the days used don’t exceed it, and amount × days used fits in 64 bits, prorate returns at most the amount.
Found before the spec was proposed: prorate(100, 1, 0) divides by zero. A large amount over a long period overflows 64 bits. The handler checked neither, so the precondition arrives with the theorem.
The team decides: reject a zero-day period at the API boundary with a 400, or keep the guarded fallback. Either way, every call inside the precondition is designed to run proven code, and the theorem says a customer is never charged more than the full amount.
Nothing formally relates the Python to the Rust.
Python integers are unbounded and // floors toward negative infinity; the port uses u64 and truncating division. The precondition is designed to keep the proven path on inputs where the two semantics coincide.
| Python | Rust port | What covers the gap |
|---|---|---|
Unbounded int | Fixed-width integers | A precondition in the spec, and the guard |
// floors toward −∞ | / truncates toward zero | They agree for non-negative operands; the precondition is designed to keep the proven path there |
| Exceptions | Result | The extension will raise the matching Python exception |
| Shared mutable lists and dicts | Owned values | Only spans with value semantics will be candidates |
str indexing by code point | UTF-8 bytes | Spans that index strings won’t be candidates in v1 |
| Duck typing | Static types | Type hints will be required; the guard rejects other types |
By design, behavior outside the proof stays exactly as it was.
Guarded ports
The patch is designed to dispatch on the approved precondition, generated as Python from the spec. Inside it the proven Rust runs; outside it the original Python runs unchanged. The guard itself will be covered by the differential tests.
The cost of the boundary
Every call into Rust pays a crossing cost. So candidates will be whole loops rather than loop bodies, every port will be timed, and a port slower than the Python it replaces will be flagged.
What will ship
The patched Python tree plus the compiled extension, built by rustproof build with maturin and stamped with the same provenance hash as a Rust project.
Your backend, with a proof on the money.
Start with one billing rule. The port will be a diff you can read, and the guard is designed to keep everything else as it was.