Every incumbent sells compute that emits numbers. FrankenSim sells the thing the numbers were always a proxy for: justified belief at minimum cost. A result is a claim that arrives with its warrant attached, not a bare float.
“A false certificate is worse than an ordinary wrong answer: a wrong answer wearing a badge.”
The entire type system exists to make that sentence impossible to violate by accident.
Before the parts, the whole. A physical question enters on the left and a certified claim leaves on the right. Cheap proposers guess, one certified test decides, the survivor accretes its evidence, claims compose, and local certificates glue into a global one. Watch a single claim run from question to proof.
a survivor accretes its certificate here once the accept test passes
the verified claim combines with a neighbouring subdomain claim
local certified claims glue into one global result over the whole domain
The expensive step runs once, on the one candidate that earned it.
Most proposals are screened for pennies and discarded. Only a candidate that passes the certified accept test pays for the confirmation solve, so the engine spends its budget where belief is actually being bought. Every stage downstream inherits the color it earned upstream: an estimate that was never certified cannot leave the machine wearing a badge.
Every quantity FrankenSim produces is stained one of three colors. The color is part of the type, not a comment. It is checked at every composition and impossible to upgrade by wishful thinking.
- verifiedinterval-certified — bounds proven
- validatedanchored to data within a regime
- estimatedbest-effort surrogate — no proof
| A\B | veri | vali | esti |
|---|---|---|---|
| veri | |||
| vali | |||
| esti |
Proven, not promised.
Bounds established by interval-certified numerics: outward-rounded intervals, exact geometric predicates, equilibrated-flux accept tests. The interval is guaranteed to contain the truth. This is the badge you can bet a bridge on.
fs-ivl · Newton–Krawczyk · Prager–Synge
Reality signed off.
Anchored to experimental data inside a stated regime: a Buckingham-π envelope where the measurement was actually taken. Trusted because it matched the world, but only where the world was asked.
fs-regime · benchmark anchors · fidelity ladder
Useful, unproven.
Best-effort: a surrogate, a coarse solve, an ML proposal. Frequently excellent, but it has shown no proof and matched no experiment. It must wear amber until something certifies or validates it.
surrogates · coarse solves · proposers
The composition rule: the weakest link wins.
Color composes like a lattice meet. Feed an estimate into a proof and you get an estimate, never the reverse. There is no operator anywhere in the 100+ crates that returns a color stronger than its weakest input. That is how FrankenSim makes laundering an estimate into a certificate a type error rather than a temptation.
Auto-demotion. A validated value silently reverts to estimated the instant it is evaluated outside the regime it was validated in. The badge is bound to its envelope; step past the boundary and the badge falls off by itself.
The color is the headline; the evidence is the dossier. Every result is an Evidence<T>: a value plus four uncertainty slices, a provenance hash, and an adjoint hook, all composed conservatively. Certified<T> is its refinement, reachable only through proof.
Discretization, rounding, and truncation error: the gap between the equation you solved and the one you meant. Bounded by interval and a-posteriori estimators.
Monte-Carlo and sampling variance carried as an anytime-valid confidence sequence, so peeking never inflates the claim.
The uncertainty of the model itself: the physics you left out. The honest, humbling slice most tools pretend does not exist.
How the answer moves as inputs move, supplied for free by the adjoint hook riding inside the value.
A content address of exactly how the value was made. explain(artifact) can always reconstruct the derivation; the result knows its own history.
A gradient rides inside the value, computed through the implicit function theorem, so sensitivity is a property of the answer, not a second pipeline.
01 fs_evidence::{Evidence, ProvenanceHash};02 03 provenance = ProvenanceHash::of_bytes(b"laplacian kernel output");04 05// A value that knows how it was made — and proves its own bound.06 drag = Evidence::exact(12.47, provenance)07 .certified() // interval-certified numerics08 .expect("exact pure-math evidence is certifiable");09 10assert_eq!(drag.value, 12.47);11// drag carries: value + interval bound + provenance + adjoint hook + cancel scopeHow do you get the speed of a guess and the trust of a proof? You let anything propose, and let only mathematics accept.
Machine learning proposes; certified numerics disposes.
A surrogate, a coarse solver, or an untrusted ML model produces a candidate in microseconds. It arrives estimated and unloved. Then a cheap, independent verifier (an equilibrated-flux Prager–Synge a-posteriori accept test) checks whether the candidate actually satisfies the governing equations to tolerance. If it passes, it is stamped verified. If it does not, it is rejected.
Untrusted, fast, plural: ML, surrogates, coarse solves. Race them all.
One cheap certified test decides. The verifier is the only thing that must be right.
No accept, no answer. A rejected speculation never leaks out wearing a badge.
The statistical slice of every Evidence<T> is an anytime-valid confidence sequence, not a one-shot interval. You may look after every sample and stop the moment the band clears the threshold, and the coverage guarantee still holds. That is what lets the e-process racer cancel its losers mid-solve without ever p-hacking the result.
Anytime-valid confidence sequence
peek at the running Monte-Carlo estimate as often as you like · stop the instant it's decisive · no p-hacking penalty
› The cyan band is an empirical-Bernstein confidence sequence (Robbins normal-mixture boundary, radius ∝ √(log n / n)) — simultaneously valid at every n, so peeking is free. The amber band is the classical fixed-n CI (±z·σ̂/√n): tighter, but only honest at one pre-committed n — peek-and-stop and its true error rate balloons (1 false exclusions of μ so far), while the confidence sequence never once lets μ escape. This is why FrankenSim can race e-processes, stop the instant a leader is decisive, and cancel the losers — with the coverage guarantee intact.
Valid at every n, not one
A classical confidence interval is only honest at the single sample size you committed to in advance. Peek repeatedly and stop when it looks good, and its true error rate balloons. A confidence sequence is a band valid simultaneously at all sample sizes, so continuous monitoring is free. The estimate can be watched, not just reported.
Racing without regret
Candidate designs each accumulate an e-value, a betting martingale. Because e-processes are anytime-valid, a leader can be declared and the losers cancelled the instant the evidence is decisive, saving core-hours at identical statistical guarantees. Optional stopping stops being a sin and becomes the whole point.
Certificates are only as good as the thing that issues them. The Gauntlet is six graded tiers that every merge must survive, and the discipline of certifying the certifiers so the judge is never above the law.
Adjointness, symmetry, conservation, d∘d = 0: the invariants a correct kernel can never violate.
The build fails if the observed convergence slope drifts more than 0.2 from the theoretical order. Silent accuracy loss is a red build.
Lid-driven cavity, Taylor–Green, NAFEMS: the problems the field already agreed on the answers to.
Relations that must hold even when the exact answer is unknown: refine, rotate, rescale, and check the invariant.
Inject cancellation mid-solve, starve budgets, race speculators. Correctness must survive the storm; resources must never leak.
Bit-identical across runs, thread counts, and instruction sets. Any divergence is a diff, not a shrug.
Certifying the certifiers. Every verifier and error estimator is itself tested against manufactured solutions with known bounds; a certificate is trusted only after the thing issuing it has passed its own Gauntlet. The Goodhart guard treats each optimizer endpoint as an adversarial example and re-checks it out of band, because a measure that becomes a target stops being a good measure.
A global certified claim is stitched from local ones. The language for when local pieces agree, when they glue into a whole, and when they cannot, is sheaf cohomology. H⁰ is the global consensus that survives; H¹ is the obstruction that names exactly why a seam leaks. Watertightness stops being something you eyeball and becomes an algebraic fact you can check.
Local claims glue when they agree on every overlap
Cover a region with overlapping charts, each carrying its own local certified value. Together they form a presheaf. They glue into a single global section, an element of H⁰, exactly when every pair agrees on the overlap they share. Nudge one chart out of agreement and the global section ceases to exist: the seam leaks. The color of the whole is the meet of the parts, so a global certificate is only ever as strong as its weakest chart.
When pairwise agreement still isn't enough
Sometimes every pair of charts is locally consistent and the pieces still refuse to glue. Transport a value around a loop of overlapping patches and it can return changed; the leftover is a cocycle, a class in H¹. Some obstructions are coboundaries, artifacts of how the patches were labelled, which a re-gauge drains to zero: pure bookkeeping, mechanically auto-fixable. Others are harmonic, a genuine topological disagreement whose holonomy is invariant no matter how you relabel. The math sorts the fixable from the fundamental for you.
A surface that seals is a theorem, not a render
Take the same machinery to geometry. Model a surface as a cellular sheaf: each patch holds local data, each shared edge holds a compatibility constraint. Watertightness is precisely the vanishing of the interface cocycle. A seal becomes something you prove, and a leak names its own location.
Watertight ≡ H¹ = 0
Watertightness is the vanishing of the first cohomology; the interface cocycle is zero. No gaps, no double walls, no self-lies. A seal is a theorem you check, not a rendering you squint at.
Conflicts classify themselves
When a merge fails, the cocycle tells you which kind of failure it is. A coboundary conflict is a bookkeeping mismatch, mechanically auto-fixable. A harmonic conflict is structural: a topological disagreement no retopo can paper over.
The most epistemically honest thing a system can do is decline, and the most useful thing it can do while declining is explain. When a request is infeasible, FrankenSim returns a structured, ranked set of ways forward instead of a stack trace.
01{02 "error": "BudgetInfeasible",03 "stage": "flux.lbm",04 "need": { "wall": "5.1h" },05 "have": { "wall": "2h" },06 "fixes": [07 { "action": "relax qoi-rel-error to 4e-2", "est_wall": "1.7h", "est_qoi_impact": "+1.8e-2" },08 { "action": "surrogate screen, certify top-4 only", "est_wall": "1.9h" }09 ]10}“A refusal that teaches is worth ten silent successes.”
A BudgetInfeasible is a conversation, not a dead end. It states exactly what the plan needed, exactly what it was given, and a ranked list of concrete fixes, each with an estimated wall-clock cost and its impact on the quantity of interest. An agent swarm reads this and re-plans; a human reads it and understands the trade in seconds. The system refuses to guess, and refuses to hide why.
None of the above is a bolt-on. The three colors, the evidence, and the refusals all fall out of ten non-negotiable principles and five things that are never, ever left implicit.
One language, Franken-constellation dependencies only. Unsafe lives only in audited leaf capsules under 300 lines, each behind a safe façade.
Bit-identical across runs, thread counts, and (best-effort) ISAs, delivered by fixed-shape reduction trees, counter-based RNG keyed by logical identity, and compensated summation.
Every operator is differentiable, certifiable, or ideally both. Gradients are checked at the merge gate; error bounds are first-class.
Every operation takes an accuracy / time / memory budget. The Error Ledger and Time Ledger compose them end-to-end and attribute every digit and every second.
Exact discrete de Rham (d∘d = 0), symplectic integrators, power-conserving ports. Preserve the math instead of resolving it away.
Kernels ship their arithmetic-intensity analysis against machine peak. No dense assembly where a matrix-free apply will do.
Cancellation is a numerical primitive. Bounded latency-to-cancel of ≤ 200 µs; speculative races kill their losers mid-solve.
Complexes and cochains, everywhere. Geometry, fields, and operators share a single typed algebra instead of six incompatible schemas.
Content-addressed artifacts, event-sourced operations, and explain(artifact): a result always knows how it was made.
The Five Explicits (units, seeds, budgets, versions, and capabilities) are never implicit, ever. Built for the swarm, compatible with humans.
Dimensional quantities are compile-time typed. A meter never silently becomes a second.
Counter-based RNG keyed by logical identity. Every random draw is reproducible by construction.
Accuracy, time, and memory ceilings travel with every call and compose across the whole plan.
The constellation is locked by hash. The kernels that produced a result are always recoverable.
The Cx context grants exactly what an operation may touch: arena, cancel token, ledger, budget.
You cannot add evidence to a value that was never designed to carry it. Composition, error bounds, provenance, and the three colors are load-bearing structure, not a reporting layer. That is exactly why they cannot be sprinkled onto a stack of six tools that only speak floats to each other.
- COMSOL
- C / Java GUI
- OpenFOAM + FEniCS
- C++
- SciPy + Dakota
- Python + C/Fortran
- COMSOL
- ✕No
- OpenFOAM + FEniCS
- ✕No
- SciPy + Dakota
- ✕No
- COMSOL
- ✕Per-solver
- OpenFOAM + FEniCS
- ✕Manual
- SciPy + Dakota
- ✕None
- COMSOL
- Project file
- OpenFOAM + FEniCS
- Case dir
- SciPy + Dakota
- ✕Ad hoc
- COMSOL
- ✕Best-effort
- OpenFOAM + FEniCS
- ✕MPI-dependent
- SciPy + Dakota
- ✕BLAS-dependent
- COMSOL
- ✕Kill process
- OpenFOAM + FEniCS
- ✕Kill process
- SciPy + Dakota
- ✕Kill process
- COMSOL
- Mesh required
- OpenFOAM + FEniCS
- Mesh required
- SciPy + Dakota
- ✕External
- COMSOL
- ✕Add-on
- OpenFOAM + FEniCS
- adjoint solver
- SciPy + Dakota
- autograd (external)
- COMSOL
- ✕No
- OpenFOAM + FEniCS
- ✕No
- SciPy + Dakota
- ✕Fixed-sample
- COMSOL
- ✕Required
- OpenFOAM + FEniCS
- ✕Required
- SciPy + Dakota
- ✕n/a
- COMSOL
- GUI / Java
- OpenFOAM + FEniCS
- dict files
- SciPy + Dakota
- Python
- COMSOL
- Proprietary
- OpenFOAM + FEniCS
- MPI stack
- SciPy + Dakota
- NumPy / SciPy stack
| Capability | COMSOL | OpenFOAM + FEniCS | SciPy + Dakota | |
|---|---|---|---|---|
| ✓One safe Rust | C / Java GUI | C++ | Python + C/Fortran | |
| ✓Certified<T> | ✕No | ✕No | ✕No | |
| ✓Composed ledger | ✕Per-solver | ✕Manual | ✕None | |
| ✓Content-addressed | Project file | Case dir | ✕Ad hoc | |
| ✓Bit-identical | ✕Best-effort | ✕MPI-dependent | ✕BLAS-dependent | |
| ✓≤ 200 µs, structured | ✕Kill process | ✕Kill process | ✕Kill process | |
| ✓CutFEM on SDF | Mesh required | Mesh required | ✕External | |
| ✓Adjoint-native | ✕Add-on | adjoint solver | autograd (external) | |
| ✓e-processes | ✕No | ✕No | ✕Fixed-sample | |
| ✓Optional | ✕Required | ✕Required | ✕n/a | |
| ✓FrankenScript IR | GUI / Java | dict files | Python | |
| ✓Franken-only | Proprietary | MPI stack | NumPy / SciPy stack |
See how seven acyclic layers turn these epistemics into running Rust, or watch them earn their keep in the three flagship pipelines.