Formal Verification

Testing checks your model against the inputs you thought of. Formal verification checks it against all inputs: Modeloop analyzes the model mathematically and proves properties about it — or shows you precisely where the proof fails. No test suite, however large, can make that statement; a proof can.

Contracts

The foundation is that every block carries a mathematical contract — a precise description of its behavior:

• What it computes. A Sum block’s output is the signed sum of its inputs; a Sin block’s output is the sine of its input. Not an approximation of the implementation — its exact mathematical meaning.
• What it requires (preconditions). Sqrt requires a non-negative input. Log requires a positive one. Asin and Acos require an input in [-1, 1]. A division requires a non-zero divisor.
• What it guarantees (postconditions). Sin and Cos always produce values in [-1, 1]. Abs is always non-negative. A Comparator is always a boolean.

Your model contributes contracts of its own, without writing anything new:

• Data types are input contracts. An input declared uint8 is guaranteed to be in 0…255; an int16 in −32768…32767. The tighter you type your interfaces, the more the verifier knows.
• Structure is a contract. Clamping a signal through a Curve block, or guarding a path with a Comparator and If-Then-Else, constrains what can reach the blocks downstream — and the verifier uses it.

What gets proven

Modeloop propagates these contracts through the entire diagram — every guarantee flowing out of one block becomes an assumption for the next — and uses an automated theorem prover to check each precondition against everything known upstream. Verified properties include:

Property	Question answered
Division by zero	Can any input ever make a divisor zero?
Math domain violations	Can a Sqrt, Log, Asin, or Acos ever receive an input outside its domain?
Numeric overflow	Can a signal ever exceed the representable range of its declared type?
Branch reachability	Are there conditional paths that no input can ever reach — dead logic hiding in the model?

Two concrete examples of how contracts compose:

• Feeding a Sin block into an Asin block is provably safe: Sin’s postcondition (output in [-1, 1]) satisfies Asin’s precondition, for every possible input.
• Feeding an unconstrained float64 input straight into a Sqrt is not provable — and the verifier says so, naming the block and the property at risk. Clamp the signal, guard the path, or tighten the type, and the proof goes through.

When it runs, and what you see

Verification runs automatically as part of code generation — it is not an optional extra pass you have to remember. The outcome is honest in both directions:

• Proven — the property holds for all inputs. Nothing to do.
• Not proven — you get a diagnostic naming the block, the property at risk, and the reason the proof failed, so the fix is local: add the missing guard, or tighten the offending type.

This is the “fail loudly” philosophy applied to mathematics: a model with an unprovable safety property does not silently ship.

Designing provable models

The verifier rewards the same habits the Modeling Guidelines already recommend:

1. Type interfaces deliberately. Every bit of range you don’t need is range the verifier must assume hostile. uint8 for a percentage beats float64.
2. Guard partial functions in the model. A clamp before a Sqrt isn’t defensive clutter — it’s the precondition made explicit, and it turns “hopefully fine” into “proven”.
3. Saturate physical quantities. Bounded signals keep every downstream overflow check provable.
4. Treat unprovable warnings as design feedback. The verifier failing to prove safety usually means a human reviewer couldn’t either — the model is missing an explicit constraint that exists only in someone’s head.

Verified code generation

Contracts also protect the step you can’t inspect by eye: the translation from model to code. Modeloop’s code generator verifies its own output —

• Equivalence checking — the generated result is mathematically checked against the source model’s contracts, so a miscompilation is caught at generation time, not on the target.
• Back-to-back validation — the reference execution and the compiled C are run on the same stimuli and cross-checked numerically.

Together with testing on the generated code (SIL/PIL), this is verification evidence designed with safety processes in mind — the kind of tool-confidence argument functional-safety standards such as ISO 26262 ask for. The claim is deliberately strong but precise: what you proved about the model holds for the code you ship, and the generator itself checks that it stayed true.