Inside a Hetu-Formal run: one proof spine, many questions
Simulation shows a property held on the stimulus you happened to run. Formal shows a property holds on every input the design can ever see, or hands you the one trace where it breaks. This is what the machine underneath a formal run is doing, and why its two most useful answers are PROVEN and a counterexample.
One reasoning core, asked eleven different kinds of question.
Formal verification has a reputation for being a different world from simulation, with its own vocabulary and its own failures. Underneath, a formal engine is doing something you can describe in one breath: it turns the design and the property into a giant Boolean question and then tries to answer it exactly. The answers it can give are narrower and stronger than a simulator's, and learning to read them is the whole skill.
The proof spine
Every Hetu-Formal application, whatever question it is asking, runs the design through the same core pipeline. The RTL becomes an and-inverter graph, a normalized gate-level form. The property and the transition relation are encoded into conjunctive normal form by Tseitin transformation. A CDCL SAT solver answers the resulting satisfiability question, and k-induction lifts that from a bounded check to an unbounded proof.
One spine. Property proof, security, datapath, safety, sequence, low-power and equivalence apps all ask their question through it.
The applications on top of this spine are just different questions posed to the same solver: property proof, cover, datapath, sequence, functional-safety, low-power, fault-tree and equivalence among them. Learn to read one result and you can read all of them, because they share the same set of verdicts.
PROVEN is a claim about every input, forever
Here is a proof result, from a committed one-click contract run:
$ hetu-formal prove -preset opentitan-aes {"verdict":"PROVEN","rule_id":"FV-BMC-000", "message":"constant-true property proved after W6 import and TS build signals=20 signal_bits=51 expressions=74 statements=18 processes=2 dual=z3 cone_state_bits=7/42 cone_inputs=5/6 cone_comb=5/7", "vacuity":{"checked":true,"assumptions_consistent":true, "antecedent_reachability":"environment_satisfiable", "antecedent_reachable":true, "reason":"constraint SAT gate proved the assume environment satisfiable; z3 confirmed the unsimplified lowered property is a tautology"}, "dual_checked":true,"dual_backend":"z3", "dual_primary_backend":"loziclibra-simplifier", "dual_secondary_backend":"z3"}
JSON wrapped for width; every field and value is verbatim from the run.
Three things in that verdict are worth slowing down on.
The cone figures, cone_state_bits=7/42, say the engine reduced the problem to the 7 state bits of 42 that the property depends on. Proving less than the whole design, but exactly the part the property touches, is how formal stays tractable.
The vacuity block is the part that stops a proof from being a lie. A property proved PROVEN is worthless if it was proved vacuously, which is what happens when the assumptions are contradictory and every property over an impossible environment is trivially true. Hetu-Formal checks that the assume environment is satisfiable and that the antecedent is reachable before it trusts the proof. A formal tool that does not vacuity-check will happily report PROVEN on a property that never had a chance to be exercised.
The dual backend line is a second reasoner, z3, independently confirming what the primary simplifier concluded. Two engines with different algorithms agreeing is a much stronger position than one engine asserting.
A counterexample is a single trace that ends the argument
Proof by itself proves nothing about the checker. So run the same contract with a mutation injected into the design and watch the verdict flip:
$ hetu-formal prove -preset opentitan-aes -mutation {"verdict":"CEX","rule_id":"FV-BMC-000", "message":"exhaustive bounded trace violates property at frame 0 dual=z3 cone_state_bits=7/42 cone_inputs=5/6 cone_comb=5/7", "witness":"{\"frames\":[{\"all_written\":true,\"arm_i\":false, \"armed_d\":false,\"armed_q\":false,\"clear_i\":false, \"new_d\":true,\"new_o\":true,\"new_q\":false, \"rst_ni\":false,\"use_i\":false,\"we_d\":true, \"we_i\":true,\"we_q\":false}]}", "dual_primary_backend":"concrete-trace-evaluator", "dual_secondary_backend":"z3-full-transition-unroll", "searches_performed":{"concrete_cex":{"bound":4}}}
JSON wrapped for width; the full frame-0 witness is shown, every field verbatim from the run.
The verdict is CEX, a counterexample, and it comes with a witness: the exact input assignment at frame 0 that drives the property to fail. This is what formal gives you that a failing simulation often does not, a minimal concrete trace that reproduces the violation with nothing extraneous around it. That witness can be written out as a VCD and opened in a waveform viewer, so the abstract failure becomes something you can step through cycle by cycle.
The pairing is the point. The same contract returns PROVEN on the correct design and CEX on the mutated one. That is the formal equivalent of the negative control in Article 01: a checker that only ever passes has not been shown to be able to fail.
UNKNOWN is an answer, and a legitimate one
Formal has a third outcome that beginners misread as failure. On a hard property the engine may exhaust its bound or its time without either proving the property or finding a counterexample. The correct verdict then is UNKNOWN, and it means precisely not decided within these limits, not passed and not failed.
This matters because the tempting mistake is to read a formal run that did not converge as if it were a pass. A tool that collapses UNKNOWN into PASS is manufacturing confidence it does not have. Hetu-Formal keeps the three outcomes distinct: PROVEN is a closed proof, CEX is a concrete failure, UNKNOWN is an open question. Only the first is signoff.
It also refuses a run it cannot ground
The same discipline appears at the front door. Point the property-proof app at RTL with no first-class assertions and it does not invent something to check:
{"verdict":"BLOCKER","rule_id":"FV-CAMPAIGN-002",
"message":"W6 IR contains no first-class assert/assume/cover records"}
A formal campaign with no properties is not a passing campaign, it is an empty one, and the tool blocks rather than returning a green result over nothing. That is the same instinct as Truti's SETUP_BLOCKED and coverage's N/A: the refusal to answer a question that was never properly asked.
PROVEN means the property holds on every reachable input, checked for vacuity and confirmed by a second solver. CEX means here is the one trace that breaks it. UNKNOWN means the question is still open. A formal tool worth trusting keeps those three apart and never lets the third quietly become the first.