A Type System for Physical Objects
The problem. Code generation became useful the moment output could be compiled and tested. The agent proposes code; the compiler tells us when that code is wrong. CAD generation has no such loop. A generated part is checked manually by a human looking at a render, or by printing the design and finding out. In industry, this review process can take weeks and errors cost millions.
Underneath this sits a deeper problem. Mechanical specifications are written in prose. Take the example below:
"Four M3 clearance holes on a 40 mm bolt circle, with walls at least 2 mm, and must not slip above 5 N·m."
That's unambiguous to an engineer, but meaningless to a machine. That's because there is no type system for physical objects.
We are building one.
Why now. CAD generation has become code generation, and only recently become good enough to make verification the bottleneck. The leading text-to-CAD systems write parametric scripts. These are programs that evaluate to CAD geometry, where an error can be traced back to the line that caused it.
Geometry, formalised. We describe geometric requirements in formal logic over the design, not the approximation used to draw it on screen. Nothing needs to be estimated, and nothing needs to be learned. Every check tells us the exact feature at fault.
mount = {h for h in Holes(part) if diameter(h) in Range(3.1, 3.3)} # M3 clearance fit
spec = All(
count(mount) == 4,
ForAll(h, mount, ForAll(e, Edges(part), dist(center(h), e) >= 5.0)),
wall_thickness_sampled_min(part) >= 2.0,
)
The same mechanical spec as before, but with the geometry made verifiable.
Holes(part) asks the CAD kernel for every full cylindrical face on the solid. Fillets are excluded automatically: rounded edges are cylindrical too, but only over a partial arc. The 3.1–3.3 mm window is the clearance fit for an M3 screw. It is wide enough to pass through, tight enough not to rattle.
The nested quantifiers are the part a checklist cannot replicate. Every hole must clear every edge, and neither count is known until the part exists. A rule engine can check fixed properties of a known shape; this ranges over whatever the generator happened to produce.
Each check returns a signed number, not a verdict. Positive is slack, negative is violation, and the magnitude is millimetres. So the output isn't "failed", it's every requirement ranked by how close it came, with the one nearest the line named first. A part that passes by 0.02 mm and a part that passes by 4 mm are different parts, and the report says so.
wall_thickness_sampled_min is named for what it is. True minimum wall thickness is a hard geometric problem; this samples, and the name says so rather than implying a guarantee it doesn't provide.
Physics, formalised. Geometry isn't enough. A torque limiter is defined by what it does in the world. So we specify behaviour as port-Hamiltonian contracts: energy-based representations of objects as systems with power-carrying interfaces. This lets us describe mathematically how objects physically interact and compose.
tool TorqueLimiter {
port handle : rotational
port bit : rotational
parameter tau_max = 5 N*m
require: always abs(bit.effort) <= tau_max # effort on a rotational port = torque
require: passive
}
The same mechanical spec, but with physical behaviour formalised.
Checking if the object is passive (never injecting energy) needs no simulation. It follows from the structure of the model, settling every scenario at once rather than sampling them one at a time. And it survives composition, which is what makes the next section work.
A port carries two quantities whose product is power. For a rotating shaft that's torque and angular velocity; bit.effort is the torque.
Notice there is no input and no output. A shaft doesn't know whether it is driving or being driven, that depends entirely on what you connect to it. Formalisms that bake a direction into the interface force you to guess, and the guess breaks when the same component is reused elsewhere in the assembly. Ports stay neutral, so a component's specification is independent of where it ends up.
always is temporal: the bound holds at every instant, not merely at the end of a test run.
passive is the one that pays. Stated plainly it quantifies over every possible behaviour of the tool, which sounds like it needs exhaustive search. In this formalism it doesn't. It follows from two properties of the declared model (the properties that stored energy has a floor, and that dissipation is never negative). Both are direct calculations on the model's structure. A claim about all scenarios becomes arithmetic.
Port-Hamiltonian systems are not ours; they come from control theory and have thirty years of literature behind them. What's new is using them as design contracts and binding them to CAD geometry.
Bridging geometry and physics. But behaviour cannot be derived from a CAD file; the same solid might be a torque limiter in spring steel but a paperweight in plastic. So we require the physics to be declared, then check that declaration against the geometry: we verify mass against the shape, a spring's stiffness against its coil dimensions, a hinge against whether it can physically turn at all.
What it is never checked against is the requirements. A binding chosen to make the requirements pass is not a verification. This is equivalent to designing a test to match the output of a program.
This scales. Verification does not restart at the assembly level. Verify a component once and we can reuse that guarantee everywhere it appears. Connect two components that never inject energy, and the assembly doesn't either. This is a proven theorem, and it holds for every such connection.[1] This produces a compounding library of certified components, which is not something a competitor can reproduce with existing techniques.
Status. So far, we've built a working geometric verifier that checks against CAD models' geometry. We're now deploying this in existing agentic CAD systems with paying users, while building the physics-based layer.
The ask. $500k for 12 months to turn our prototype into a commercial proof of concept. In short, this covers: deploying our product in existing CAD software with paid users; building partnerships with text-to-CAD companies, where we offer both training and agent infrastructure; mapping our verification certificates onto legally binding certificates, extending our product to industries such as aerospace and medical hardware design.
Contact Me · oli(at)oliverpryce.xyz
van der Schaft, A. J. L2-Gain and Passivity Techniques in Nonlinear Control. Springer, 2000. The compositionality of passive systems is a central result of port-Hamiltonian theory. ↩︎