Most smart-contract vulnerabilities aren't exotic— they're an off-by-one in accounting, a > that should have been >=, or an invariant quietly broken after one mutator. Tests catch these only if you happen to test the exact input that breaks them. Dhruv Rastogi wanted something stronger: either a proof that a property holds for every possible input, or a concrete counterexample showing exactly where it fails. The catch? He built the entire proving core himself, with no Z3, no JavaSMT, and no external solver dependency.

Why Drop SMT Solvers Altogether?

Rastogi wanted to understand symbolic execution and decision procedures from first principles rather than treating an SMT solver as a black box. Traditional formal verification tools like Certora or Halmos rely on mature SMT backends— powerful, but opaque. By building his own core in the DhrLang project (github.com/dhruv-15-03/DhrLang), he could see exactly where every proof came from and maintain full control over soundness guarantees.

How contract prove Works

The tool annotates functions with specification markers: @requires for preconditions, @ensures for postconditions, and @invariant for contract-wide properties. When you run dhrlang contract prove --bound=8, the prover returns exactly one of three verdicts— PROVED (true for all inputs), REFUTED (with a reproducing counterexample), or UNKNOWN (it can't decide). That third verdict is load-bearing: the design philosophy prioritizes honesty over coverage. It will never claim PROVED without a real proof, and never says REFUTED without a confirmed concrete failure.

The Linear Arithmetic Trick

Terms are represented as immutable linear forms— constant plus a sum of coefficients times atoms. Only operations that preserve linearity (add, subtract, negate, multiply/divide by constants) stay in the form. Genuinely non-linear expressions like a * b get folded into opaque atoms: interned identifiers representing "some 256-bit value I won't reason about further." The clever part is atom interning— structurally identical opaque terms share the same key. This means result == a * b cancels out on both sides through pure linear reasoning, even though the prover never multiplies two unknowns.

Decision Procedure: Fourier-Motzkin Elimination

To decide whether hypotheses imply a goal, Rastogi checks if hypotheses ∧ ¬goal is unsatisfiable. He builds a system of linear constraints (each hypothesis, the negated goal, and one atom ≥ 0 row per atom for uint256 domain) then projects atoms out using Fourier-Motzkin elimination. If the system collapses to a bare constant < 0, it's contradictory— meaning the negation is impossible, so the spec is PROVED. Why this is sound: a system with no rational solution has no integer solution either, so rational-UNSAT implies integer-UNSAT.

Zero False Positives Through Fuzzing

When the prover finds something suspicious (like @ensures(result > a) on an add function), it doesn't report REFUTED immediately. Instead, it hands candidates to DhrLang's existing concrete spec-fuzzer (the L3 engine), which executes the function and reproduces the violation before confirming the verdict. The fuzzer acts as ground-truth oracle— eliminating false positives entirely.

Deliberate Limitations

Loops make postconditions UNKNOWN. Mapping aliasing, external calls, and nonlinear combinations collapse to UNKNOWN. Rastogi is upfront about these boundaries: this is experimental (L2b), not production-ready, and it's explicitly not a Certora or Halmos competitor. Those are mature tools verifying real Solidity in production. This is a from-scratch exploration meant to understand the metal underneath.

Key Takeaways

  • Three annotations (@requires, @ensures, @invariant) plus an arithmetic-mode marker define contract specifications
  • Fourier-Motzkin elimination over linear forms replaces traditional SMT solving for a class of properties
  • Opaque atoms with structural interning handle non-linear operations without leaving the linear decision procedure
  • Bounded concrete search + spec fuzzing eliminates false positives when generating counterexamples

The Bottom Line

Rastogi's approach proves that you don't need an industrial-strength SMT solver to get sound verification for a meaningful class of EVM contract properties. The discipline of saying UNKNOWN rather than overclaiming is exactly the kind of engineering integrity this space needs more of— especially after watching DeFi lose billions to bugs that basic formal methods could have caught.