Certificates ride inside values
Every result is an Evidence<T> — a value plus four uncertainty slices (numerical, statistical, model-form, sensitivity) that compose conservatively. FrankenSim returns proofs, not just numbers.
Evidence
v0.0.1 · 54 crates · pure Rust
Simulation
that returns proofs.
FrankenSim is a single, memory-safe Rust continuum for geometry, physics, optimization, and rendering — where derivatives, error bounds, budgets, provenance, and cancellation ride inside the values.
click a layer to inspect · trace a request to see dataflow
fs-qty · fs-obs · fs-evidence
▽ Franken constellation — asupersync · FrankenSQLite · FrankenNumpy · FrankenTorch · FrankenScipy
L0–L6One acyclic workspace
- 7
- 54
- 106K
- 855
L0 Substrate → L6 Helm
one acyclic workspace
pure, memory-safe, Franken-only deps
+ 82 conformance suites
The Continuum
Geometry, physics, optimization, and rendering usually live in six incompatible tools, and the seams between them are where correctness drowns. FrankenSim makes derivatives, error bounds, budgets, provenance, and cancellation first-class values that travel together.
L2 · Morph
The RegionRegionAn abstract measurable subset of ℝ³The founding move of the geometry kernel. A Region is an abstract subset of space that is never stored directly — it is only ever presented by Charts. Physics, optimization, and rendering all speak about Regions, so no single representation is privileged., and its ChartsChartA concrete representation of a RegionA concrete presentation of a Region: an SDF grid, a half-edge mesh, an F-rep CSG tree, a NURBS patch, a voxel field, or a neural field. Charts of the same Region must agree — chart agreement is a checkable proposition, not a hope.
A Region is an abstract subset of space that is never stored directly. It is only ever presented by Charts — an SDF, a mesh, an F-rep tree, a NURBS patch, a voxel field. No representation is privileged, and charts of the same Region must provably agree.
When one task holds a Region as an SDF and another needs a mesh, the Rep RouterRep RouterPareto shortest path over chart conversionsGiven a Region in one Chart and a task that needs another, the Rep Router solves a Pareto shortest-path problem over the graph of chart-to-chart conversions, choosing the cheapest chain that respects the error budget — and every conversion emits a certificate. solves a Pareto shortest-path problem over the graph of conversions, picking the cheapest chain that respects your error budget — and every hop emits a certificate.
Evidence
The certificate rides inside the valueEvidence<T>A value plus its uncertainty and provenanceThe core wrapper. Evidence<T> (and its certified refinement Certified<T>) carries a value plus four uncertainty slices — numerical, statistical, model-form, and sensitivity — that compose conservatively, together with a provenance hash, an adjoint hook, and a cancellation scope. A result always knows how it was made.
A FrankenSim result is not a bare number. Every value is an Evidence<T>: the number plus four uncertainty slices — numerical, statistical, model-form, and sensitivity — that compose conservatively, alongside a provenance hash and an adjoint hook.
Because the bound travels with the value, composition can never quietly lose it. FrankenSim doesn't just return answers; where it matters, it returns proofs.
Epistemics
Three colors, no launderingThe Three Colorsverified / validated / estimatedFrankenSim's epistemic type system. A quantity is verified (its bounds are proven by interval-certified numerics), validated (anchored to experimental data within a stated regime), or estimated (best-effort). Composition is type-checked so an estimate can never be laundered into a certificate, and a validated value auto-demotes to estimated the instant it leaves its regime.
Every quantity is typed one of three colors: verified (interval-certified), validated (anchored to experiment), or estimated. Composition is type-checked, so an estimate can never be laundered into a certificate.
A validated value auto-demotes to estimated the instant it leaves its regime of validity. A false certificate is worse than an ordinary wrong answer — it is a wrong answer wearing a badge — and the type system exists to make that impossible.
L3 · Flux
FEM-grade physics on a raw SDFCutFEM-on-SDFFEM-grade physics on a level setThe marquee bridge between geometry and physics: finite-element accuracy computed directly on a signed distance field, with certified cut cells, ghost penalty, and Nitsche boundary conditions — and zero body-fitted meshing in the loop.
The marquee bridge between geometry and physics: finite-element accuracy computed directly on a signed distance field. Cut cells get a ghost penalty and Nitsche boundary conditions; the interior integrates exactly.
There is zero body-fitted meshing in the loop — so the optimizer can reshape the boundary every iteration without ever regenerating a mesh.
Adjoints
Differentiate through the solutionAdjointDifferentiate through the solutionFrankenSim computes gradients via the implicit function theorem — differentiating through the converged solution rather than unrolling solver iterations — so sensitivities are exact and cheap, and gradient checks gate every merge.
To get the gradient of an objective with respect to thousands of design parameters, FrankenSim solves the physics forward once, then solves a single adjoint problem via the implicit function theorem — not by unrolling solver iterations.
The full gradient comes back at roughly the cost of one extra solve, regardless of parameter count. Gradient checks gate every merge, so the derivatives are always exact.
The Flywheel
Certified speculationCertified SpeculationUntrusted proposers, a certified verifierThe system's single research bet: cheap, possibly-wrong proposers (surrogates, coarse solves, ML) generate candidate answers, and a cheap certified verifier — an equilibrated-flux, a-posteriori accept test — either stamps a candidate verified or fails closed. Machine learning proposes; certified numerics disposes.
The single research bet. Cheap, possibly-wrong proposers — a surrogate, a coarse solve, an ML guess — fire candidate answers at high rate. A cheap certified verifier, an equilibrated-flux a-posteriori test, either stamps a candidate verified or fails closed.
Machine learning proposes; certified numerics disposes. Most candidates are screened for pennies; only survivors pay for the expensive confirmation.
L4 · Ascent
Race designs, stop when decisivee-processAnytime-valid evidenceA betting martingale that stays statistically valid no matter when you stop or how often you peek. FrankenSim uses e-processes and confidence sequences to race candidate designs and stop the instant the evidence is decisive, under optional stopping.
Candidate designs are evaluated concurrently, each accumulating an e-value — a betting martingale. Because e-processes are anytime-valid, you may peek continuously and stop the instant a leader crosses the threshold, with no p-hacking penalty.
When a winner is declared, the losers are cancelled mid-solve — saving 2–5× the core-hours at identical statistical guarantees.
P2 · Marquee
Topology optimization, no mesh in the loopSIMPSolid Isotropic Material with PenalizationThe density-field parameterization behind topology optimization: a continuous material density per cell, penalized toward solid-or-void, differentiated through the physics via the adjoint.
The forcing function for the whole geometry-physics bridge: a density field evolves to minimize compliance under a volume fraction, its physics computed by CutFEM directly on the level set.
A grey blob resolves into a classic cantilever truss — and every iterate carries a composed error certificate, with the mesh-step counter pinned at zero.
L0 · Substrate
Two lanes, ≤ 200 µs to cancelTwo-Lane ExecutorLatency lane + throughput laneThe heart of L0. A latency lane (async orchestration, ledger I/O, progress) runs alongside a throughput lane (a work-stealing fork-join pool whose units of work are tiles), targeting a bounded latency-to-cancel of ≤ 200 µs and supporting speculative races and resumable solvers.
A latency lane handles orchestration, ledger I/O, and progress while a throughput lane runs a work-stealing pool whose units of work are tilesTileThe unit of scheduling and determinismThe atomic unit of work in the throughput lane: a cache-aligned block whose lifetime is a cancellation scope and whose reduction shape is fixed, making parallel results deterministic and cancellation prompt.. Conversational responses stay under 100 ms even under full load.
Cancellation is a numerical primitive: a cancel token stops in-flight tiles within a bounded 200 µs, and speculative races kill their losers the moment a winner lands.
Determinism
Bit-identical, every timeTileThe unit of scheduling and determinismThe atomic unit of work in the throughput lane: a cache-aligned block whose lifetime is a cancellation scope and whose reduction shape is fixed, making parallel results deterministic and cancellation prompt.
A naive parallel sum wobbles in its last bits depending on how threads happen to interleave. FrankenSim uses fixed-shape reduction trees, counter-based RNG keyed by logical identity, and compensated summation.
The result is bit-identical across runs, thread counts, and — best-effort — instruction sets. Reproducibility is a side effect, not a virtue you have to chase.
L6 · Helm
A campaign you can queryThe Design LedgerThe FrankenSQLite system of recordBuilt on FrankenSQLite: content-addressed artifacts, event-sourced operations (the Five Explicits), lineage, metrics, a tune cache, and tombstones — with time-travel, forkable worlds, and explain(artifact). It makes a six-month campaign a database you can query instead of a directory you fear.
Every artifact is content-addressed and every operation is event-sourced with its Five ExplicitsThe Five Explicitsunits, seeds, budgets, versions, capabilitiesThe five things that are never implicit in FrankenSim. Every operation states its units, its random seeds, its accuracy/time/memory budgets, the versions of the kernels it used, and the capabilities it was granted. This is what makes the system safe for an agent swarm to drive.. Artifacts form a lineage DAG you can time-travel through, fork into parallel worlds, and interrogate with explain(artifact).
The Design Ledger is what turns a six-month design campaign into a database you can query instead of a directory you fear.
The Gauntlet
Nothing merges without proofThe GauntletThe tiered correctness program (G0–G5)The graded suite every merge must pass: G0 property and algebraic-law tests; G1 manufactured solutions and order verification (the build fails if the observed convergence slope deviates from theory by more than 0.2); G2 canonical benchmarks; G3 metamorphic tests; G4 chaos and cancellation storms; G5 determinism and cross-ISA divergence audits — plus certifying the certifiers.
Six graded tiers gate every merge: property laws, manufactured-solution order verification, canonical benchmarks, metamorphic tests, chaos and cancellation storms, and cross-ISA determinism audits.
If the observed convergence slope drifts more than 0.2 from theory, the build fails. Repository policy is code too — the layer direction and the Franken-only dependency rule are enforced mechanically.
Why FrankenSim
Not a faster solver bolted onto old plumbing — a ground-up continuum where the value that flows through the system already carries its own proof, budget, and provenance.
The three-color type system
Every quantity is verified (interval-certified), validated (anchored to experiment), or estimated. Type-checked composition means an estimate can never be laundered into a certificate.
Epistemics
Determinism by construction
Bit-identical across runs, thread counts, and ISAs. Fixed-shape reduction trees, counter-based RNG keyed by logical identity, and compensated summation make reproducibility a side effect.
Substrate
Adjoint-native gradients
Differentiate through the solution via the implicit function theorem — not through solver iterations. Gradient checks are a merge gate, not an afterthought.
Differentiation
Geometry as Region + Chart
A Region is abstract; Charts (SDF, mesh, F-rep, NURBS, voxel) present it. The Rep Router solves a Pareto shortest path over conversions, respecting your error budget and emitting a certificate.
Morph
CutFEM on a raw SDF
FEM-grade physics directly on a level set — ghost penalty, Nitsche BCs, certified cut cells — with zero meshing in the loop. The marquee bridge between geometry and physics.
Flux
Anytime-valid statistics
e-processes and confidence sequences give valid inference under continuous peeking and optional stopping. Race candidate designs and stop the moment the evidence is decisive.
Ascent
The Design Ledger
Content-addressed artifacts, event-sourced operations, and explain(artifact) turn a six-month campaign into a database you can query instead of a directory you fear. Time-travel and forkable worlds included.
Helm
Roofline-honest kernels
Every kernel ships its arithmetic-intensity analysis against machine peak. Targets are stated so they can be failed — GEMM ≥ 75% of peak, SpMV ≥ 85% of STREAM, LBM ≥ 1.0 GLUP/s.
Performance
Structure-preserving physics
Exact discrete de Rham (d∘d = 0), symplectic and Lie-group integrators, and power-conserving ports. Preserve the mathematics instead of resolving it away.
Flux
Certified speculation
Untrusted fast proposers generate candidates; a cheap certified verifier accepts them or fails closed. Machine learning proposes; certified numerics disposes.
The Flywheel
Pure, safe, Franken-only
One memory-safe Rust workspace, zero runtime dependencies outside the Franken constellation. Unsafe lives only in audited leaf capsules under 300 lines, each behind a safe façade.
Foundations
The Archipelago
The incumbents assume a human absorbs the seams between solvers. FrankenSim makes composition itself a first-class certified operation — the one thing they cannot retrofit.
| 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 |
The Interface
Agents and humans drive FrankenSim through FrankenScript — a typed IR where units, seeds, and budgets are stated inline, and every refusal teaches.
studies/spout-laminar-v3.fscript
01(study "spout-laminar-v3"02 (seed 0x5EED0001) (versions (constellation :lock "2026-07"))03 (budget (wall 2h) (mem 96GiB) (qoi-rel-error 2e-2))04 05 ; geometry: a revolved Chebyshev profile with a filleted lip06 ( vessel (frep (revolve (cheb-profile "body.chb"))07 (fillet :edge lip :r 3mm)))08 09 ; physics: a free-surface pour, tilted over 3 seconds10 ( pour (flux.free-surface-lbm vessel11 (fluid :model (carreau :mu0 0.12Pa*s :n 0.8) :sigma 0.061N/m)12 (schedule :rate 0.5L/s :tilt (ramp 0deg 65deg 3s))))13 14 ; optimize the lip lever pour stability, stop when decisive15 (ascent.optimize J :over lever :method (lbfgs :m 17)16 :until (any (grad-norm 1e-5) (e-value 20) (budget-exhausted))17 :emit (pareto ledger report)))Syntax_Validation_Active
UTF-8_ENCODEDexamples/laplacian.rs
01 fs_sparse::{Coo, Csr};02 03// Assemble a 1-D Laplacian, deterministically.04 coo = Coo::new(3, 3);05coo.push(0, 0, 2.0);06coo.push(0, 1, -1.0);07coo.push(1, 0, -1.0);08coo.push(1, 1, 2.0);09coo.push(1, 2, -1.0);10coo.push(2, 1, -1.0);11coo.push(2, 2, 2.0);12 13 csr: Csr = coo.assemble(); // fixed-shape, order-independent14 y = vec![0.0; 3];15csr.spmv(&[1.0, 2.0, 3.0], & y); // bit-identical on 1 or 96 cores16assert_eq!(y, vec![0.0, 0.0, 4.0]);Syntax_Validation_Active
UTF-8_ENCODEDThe Build Log
Each phase gate is a Gauntlet state, not a date. The vertical skeleton, Bedrock, and Geometry are proven; the first optimization is landing now.
PV
The Vertical Skeleton
Proved the typed continuum end-to-end: 2D SDF → PDE → objective → adjoint → optimize → replay
Established the Cx execution context and the Design Ledger v0
Locked the Franken constellation by hash
Runtime Log v0.2
P0
Bedrock — the numerical floor
BLIS-style GEMM, batched small-dense, sparse formats with deterministic assembly, FFT
Certified interval / Taylor arithmetic and exact geometric predicates
Counter-based Philox RNG and QMC keyed by logical identity
Two-lane executor with ≤ 200 µs latency-to-cancel; G0 + G4 green
Runtime Log v0.2
P1
Geometry + Eyes
The Region / Chart abstraction and the Rep Router over SDF / mesh / F-rep / NURBS / voxel
Dual contouring, incremental Delaunay, generalized winding numbers, certified round-trips
The Lumen preview tracer: sphere-traced turntables at target ray rates
Runtime Log v0.2
P2
Elasticity + First Optimization
FEEC elasticity, CutFEM-on-SDF, matrix-free p-multigrid + smoothed-aggregation AMG
Adjoint-native gradients with a merge-gate gradient check; SIMP density fields
The marquee: topology optimization on a raw SDF with a composed error certificate
Runtime Log v0.2
FrankenSim is a large, working Rust workspace — 54 crates, ~106K lines, 855 tests. There is no crates.io release yet; build it from source and read the plan.
terminal
$
git clone github.com/Dicklesworthstone/frankensimMIT License · Pure Safe Rust
Get Started