Every page names the published work it builds on and links the evidence file it was checked against. All of it is simulation or proof inside a stated model; nothing here is measured on silicon. Every file this site publishes is listed with its size and checksum.
Founder: Nick Harris. AI agents do our research and engineering. Each result page says how it was checked: against an outside solver, by an interval-arithmetic proof, by a Lean-checked step, or against our own simulator; these checks ran on our own machines. Who we are · How the work is checked
A coupling predictor, graded on capacitance by outside solvers
Graded by FastCap, an outside solver, our predictor beat a simple add-up-the-pairs baseline on each of three samples of layouts; the spread is not reported.
A printing check whose range contained our own simulation at every pixel tested
For each pixel of our simulated print, a computed range contained our own simulation in every check of a battery of test masks.
The capacitance a flat model of a via leaves out, simulated in three dimensions
Flat models of a via leave out the capacitance at its two ends; our own three-dimensional solver computed that share in simulation, and one flat solver now adds it back.
A proved floor on how far the add-up-the-pairs shortcut overstates coupling
Inside our simplified model of the vias, adding up coupling one pair at a time over-predicts the worst coupling for every layout in one family.
Small mask edits, re-checked without starting over
After one small mask edit, a computed bound shows some nearby tiles are still valid without re-simulating them.
Wiring models built so that, in exact arithmetic, they cannot create energy
Wiring models whose gain, in exact arithmetic, never exceeds one and whose response is the same in both directions, for any parameter values.
Proved checks on a neural stand-in, and the one that fails
Proofs that a neural stand-in for our impedance solver stays in range, moves the physically right way and stays smooth, with the one check that fails stated.
A layout search gated by a re-computed physics check
An automated via-layout search through glass in which every candidate must pass an isolation check re-computed by a separate solve.
The arithmetic behind our statements about whole families of layouts
Arithmetic on ranges that rounds every step outward, so a statement over a whole family of layouts is proved rather than sampled, under stated floating-point assumptions.
A design-check certificate that records its inputs, model and bounds
A compact record of a design check that names its inputs and its model, and states each number with a range or a note of how it was obtained, beside the verdict.
Choosing which rigorous printing simulations to run, against a proved floor
A method that picks which designs to run through a slow, rigorous printing simulator, with a proved floor on how few picks from its candidates could cover the same region.
A proved floor and ceiling on screening for one via family, and a proved direction between two spacings
For one family of via layouts, interval proofs bound the many-body screening from both sides, and prove that the closer of two stated spacings screens more, in a simplified model.
A cache for printing-check proofs, tested against forged inputs
A cache for slow printing checks, built to hand back a stored result only when its input fingerprints match; it refused every forged input in our planted tests, and it once served a stale result.
Passive circuit models from our extraction, checked by an outside tool
Extracted results written as Touchstone models made passive by enforcement and checked with scikit-rf on the tested case, with the training-data leakage under our impedance figure published.
A fast predictor that answers only when a bound admits it
A fast stand-in for our coupling solver that answers only when a bound on its own error admits the answer, and otherwise refines or escalates.
Proving an impedance target is reachable before promising a geometry
Before an optimizer promises a via geometry, the impedance target is proved reachable by our stand-in model, and the geometry is returned as a certified interval or refused.
Where an add-up-the-pairs baseline flips signoff verdicts, in simulation
What the add-up-the-pairs coupling shortcut costs at signoff: a searched worst case, a measured pass or fail flip rate, and a large field solved by declining to answer when unsure.
Some statements behind our bounds, checked by an SMT solver that must refute planted false claims
Some of the statements behind our bounds ship as executable proofs, checked by an SMT solver that must refute planted false claims; the family-wide bounds rest on interval proofs instead.
In one recorded run of test coupons, a public tool's default fit failed the passivity test; ours passed
On every de-embedded coupon tested, a public library’s default circuit fit is non-passive under the IEEE interconnect test, and our passive-by-construction synthesis passes.
One guard via between a tight pair, with a proved floor and ceiling on its screening
For every layout of a tight pair with one guard via, an interval proof bounds the guard’s screening from both sides, in a simplified model.
How far our frozen field solver is from the exact answer, measured
The discretisation error of our frozen field solver, measured against an exact closed form, a high-precision anchor and a continuum truth of the same model.
Design gradients through a coupled electrical and thermal solve, checked against finite differences
The gradient of a package’s joint electrical and thermal answer, computed through the joint solution and checked against finite differences in a three-dimensional model.
A dependency-free verifier for our compiled design kit, tested on forgeries it generates
A checker for our compiled design kit that runs on plain Python and rejects every forged kit it generates, so it can be seen to fail.
Where three common coupling shortcuts are safe, and where they are not, mapped over a stated range
Maps of where three common coupling shortcuts err on the safe side and where on the unsafe side, over a stated range of dimensions.
A design contest's scoring, attacked by cheating entrants, and what got through
A chiplet design contest whose scoring was attacked by cheating entrants, with the hole that shipped, its fix and what still gets through.
Printing checks on tiles of a mask, combined into one check for a region
Per-tile printing checks combined into one check for a whole region by a Lean-checked step, with a measured allowance for spill between tiles.
Error control around a fast stand-in, so that unsure answers go to the full solver
A fast stand-in for our solver answers only inside a distribution-free error bound, and unsure cases go to the full solver.
A joint design decision without either side handing over its input, with the leaks we found in it
A protocol, tested on our own files, for two parties to reach a joint design decision without either handing over its input, with the leaks found in the published files.
Six bets that lost, published with the criteria fixed before they ran
Six approaches that failed criteria written down before they ran, published with the criteria and the numbers.
How a buyer can run our software today, including the parts that are not checked
The ways a buyer can run our software today, with the three replay checkers that pass and the parts that have no check.
A licensing demo that fails if its independent check ever stops disagreeing with the protocol
A licensing demo for chip designs that stops with an error if its independent check ever stops disagreeing with the protocol.
An outside check that sees every private design at once, used to test a confidential protocol
A test-only check that joins every private test design and answers directly, to test a protocol in which no party sees the others’ designs.
Known ideas, listed without a page
- The record claims, inside our simplified model of one family of via layouts, a computer proof that no model which adds coupling up one pair at a time can match the full coupling for every layout in the family; its evidence file is linked here, and the result has no page of its own. That coupling is not pairwise-additive is textbook electrostatics; what we add is a proved, and small, distance over the whole family. It bounds only models that add coupling up one pair at a time. Evidence file
Not yet published
This result has no page yet, because the file it rests on does not yet state its limits in a form we can publish. Until it does, we make no claim for it here.
- A floor on the printing error for a very small mask-design problem, reported by an off-the-shelf optimisation solver.
How the work is checked
- Graded by solvers we did not write
- Our lead result is scored by FastCap and Palace, two public field solvers. In the fairest test FastCap sets both the baseline and the right answer, on 24 generated test layouts (the record calls them held-out but does not say from what), of which it counts 21 as its confirmatory set.
- Open-source checkers
- 35 open repositories, datasets and live demos, each link fetched when this page was built. The checkers are open; the solver runs behind the results are not.
- Proofs written in Lean
- The theorems marked Lean in Theorems & Bounds on the home page have their stated step written in Lean, a proof checker, and the Lean files are published as written; the build records we publish are listed on the page about our solver-checked statements, which names the one file that has none. For the passive wiring models, that step is the core algebra lemma, not the whole argument. The other theorems are computer proofs by interval arithmetic.
- A method that publishes its misses
- We publish limits beside successes: our mask-edit method is established for single edits, not for chains of edits.
Questions, answered plainly
- What is a chiplet?
- A chiplet is a small chip designed to be combined with others inside one package, instead of putting everything on a single large chip. The package then matters as much as any one piece: the carrier underneath (an interposer) and the many tiny vertical wires through it decide whether the pieces work together.
- What does ChipletOS actually do?
- ChipletOS is a research effort. It publishes checked results on printing chip patterns and on the coupling between vertical connections in package carriers. Its work on trusting a chip you cannot open up, and on glass interposers, is not yet published beyond the bounds shown. It is not a released product and not a running service.
- What does “machine-checked” mean?
- For some results, a stated algebra step (for the passive wiring models, one standard lemma) is written as a proof in a proof assistant called Lean, and a program checks every step of that proof. The argument that connects those steps to the full result is summarised on the result’s page and is not itself machine-checked. Others are computer proofs by interval arithmetic, or measurements graded against outside solvers. Each result says which kind it is, and what it does not claim.
- What is FastCap, and why use it as a judge?
- FastCap is a public three-dimensional field solver that we did not write; we chose its layouts and settings and ran it ourselves, and the runs are recorded by fingerprint only. We compare our predictor and the add-up-the-pairs shortcut against its answers on the same layouts. It grades capacitance only, and it is a simulation, not a measurement on silicon, so the comparison says how close we come to a trusted solver, not how a built package behaves.
- What is coupling between vias, and why does it matter?
- A via is a tiny vertical metal connection through the carrier. Neighbouring vias act on each other electrically, and that coupling affects whether signals arrive cleanly. Design tools estimate it so teams can set spacing and margins before anything is built.
- What is the add-up-the-pairs shortcut?
- A quick way to estimate the coupling in a group of vias works out each pair on its own and adds the results. It is quick, but the pairs also interact through their neighbours. For one family of closely spaced vias, inside a simplified model of the vias, we prove that the shortcut overstates the worst case by at least a stated minimum.
- Is this about real hardware?
- Not yet. The proofs are about models, and each result states which model. Against our own boundary-element solver, the gap is measured, not proved. Our checks ran on our own machines, and we make no claim about physical measurements of glass vias.
- Can I check the work myself?
- Partly. You can confirm that each file is the one we cite: every figure links to its file, and the checker on the home page confirms, in your own browser tab, that a file matches the checksum this site publishes for it. That checks fingerprints, not the physics. The solver runs behind the comparisons are recorded only by fingerprint and cannot be re-run from this site. Where a result is measured rather than proved, the page says so.
- Who is ChipletOS for?
- Chip-package and interposer design teams, makers of extraction, signoff and lithography software, and the diligence teams that examine them. To license or acquire a result, or to ask about one, write to the address at the bottom of the page.