How a rule is made
A rule you can check, not a rule you are asked to trust.
Mathematical Autopsy is the method — a fixed sequence a rule must survive before it is allowed to exist. The Mathematical Autopsy Engine is the software that runs it and refuses to skip a step. Skip one and the package does not exist; that is enforced by the recertification record inside every brick, not by anyone remembering.
One rule
From a sentence to something that can refuse.
Both the prover and the oracle must say GO, or there is no package.
The Oracle
Where the loop closes.
A proof tells you the specification is sound. It does not tell you that the executable rule still behaves like the specification. That step is where this industry relies on testing, and says so.
So we check it, in the only way worth anything: the cases are derived from the contract, never from the generated code, and the artifact is forbidden from grading itself — a schema constraint, not a convention. The prover and the oracle must both return GO. If either refuses, there is no package.
The limit, stated the way the receipt states it: this is finite scenario equality bounded by the declared oracle cases. It is evidence, not a universal refinement proof.
What is new, and what is not
This is the claim most likely to be challenged by someone who knows the field, so it is split precisely.
Not new
- Oracles derived from a specification rather than an implementation — there were 317 papers on that by 2015.
- Verification independence, which DO-178C has required for decades.
- Back-to-back testing of a model against generated code, highly recommended under ISO 26262 at the higher safety levels.
- Shipping evidence with an artifact, which is proof-carrying code from 1997.
Genuinely thin in the literature
- Hash-locking the original human intent as the root of the chain — the least-populated part of the space.
- Binding a proof result and an execution result into one signed receipt keyed to that intent, for which the attestation ecosystem has no predicate at all.
- Making the oracle's independence a machine-checkable property — these scenarios came from the contract hash, not the artifact hash — rather than an organisational rule about which human wrote them.
None of the six steps is new. The composition, the gate semantics and the receipt are.
And it matters more now than it would have five years ago, because the author of the artifact is often a model. Tests written after a model's own code catch about 14% of faults; tests written from the specification catch about 25%. Implementation-derived invariants caught three bugs out of a hundred and one, and got two of those wrong.
Scope
What it can turn into a rule — and what it will not.
The subject matter is open. The shape is deliberately narrow, and the narrowness is what makes the proof possible.
It builds
Threshold and arithmetic decisions, bounded state machines, admission and classifier and monitor families, embedded control components, and compiled decision graphs. A disclosure limit, a lending decision, a sanctions screen, a seller's approval workflow — each of those is a bounded decision structure wearing business clothes.
It will not build
Arbitrary programs, unbounded processes, free-form formulas outside its typed language, or anything that reads the wall clock. We publish that list, because a tool that claims to do everything has told you nothing about what it does.
What comes out
The brick.
A rule leaves the engine as a signed package. The one shipping today carries the constructed calculus, a Lean 4 proof manifest, the proof itself, six machine-checked invariants, a scorecard, a conformance record, provenance, signatures over both payload and manifest, and a digest for every asset inside. The control plane refuses to admit it if any of that fails to check.
Every brick also declares, in machine-readable form, what it does not prove. Our data-minimisation candidate names GDPR Article 5(1)(c), then states that the domain is reduced to a single boolean, that it proves an admission decision over that boolean and nothing further, and that purpose-binding, field-level necessity, retention and proportionality are not proved.
A proof that does not state its boundary is not a proof. It is a reassurance.
Those 671 are proposed candidates, held rather than published. The run was a demonstration of the method, not a shipped rule set.
Start at one seam
See a rule built, then see it refuse something.
The shortest useful version of this is not a deck. It is watching one rule go from an English sentence to a package, and then watching the action gate refuse something on the strength of it.