When the proof gate met Solidity

Our web-app proofs run against a live database. We boot a real Postgres, attack the generated app, and watch the database refuse the attack — tenant isolation, invariants, append-only ledgers, every one checked by experiment. It works because there’s a runtime to interrogate.

Smart contracts raise the stakes and take away the safety net. A bug doesn’t wait for the next deploy. It’s immutable, on-chain, and usually sitting on money. So the question was obvious: could the same proof discipline point at Solidity? It could — and on-chain we can do something better than testing.

A test checks the inputs it happens to try. Even a good fuzz test is still sampling. Against a real database that’s the strongest honest signal you’ll get, but a contract gives you a sharper tool: symbolic execution. Instead of running a function on a thousand concrete inputs, a symbolic engine reasons about all of them at once and asks whether any input, anywhere in the space, can break the property.

That’s the formal-methods work we’d called the deepest thing on the roadmap. Contracts are where it pays off first: the surface is small, the properties are crisp, and the stakes are absolute. The gate runs Foundry’s fuzzer and invariant runner for breadth, then hands each check_* property to Halmos to prove over the whole input space. A property that holds for every input is a different category of evidence than a sample that happened to pass.

Paste a contract, or compile one straight from an ISL spec, and the prover drives a real toolchain end to end:

# 1. scaffold a throwaway Foundry project
   foundry.toml + src/<Contract>.sol
   lib/forge-std + lib/halmos-cheatcodes

# 2. prove
   proveContract()  →  ingest → encode → emit harness
                        Halmos (symbolic) → non-vacuity check

# 3. bind to the deployed code
   keccak256(deployedBytecode)   via  cast keccak

# 4. issue the certificate
   buildProofCertificate()  →  signed, bytecode-bound

The properties it discharges out of the box:

Those ten are the mature set — the mechanical safety most tooling already targets. The interesting question was whether the same harness could reach the risks people assume formal methods can’t touch: oracle manipulation, governance, MEV. We built six new properties on the exact same substrate, and we held each to a hard bar. The prover has to prove a guarded contract and refute a broken twin with a real counterexample. Nothing earns a checkmark on its word.

Four prove and refute cleanly today: deadline, slippage, timelock, quorum. Each one proves the safe contract and hands back a concrete counterexample on the broken one — a swap that credits less than the user asked for, a proposal that executes below quorum, an action that fires before its timelock. Oracle catches the manipulation too: it refutes a contract that an adversarial price can drain.

Snapshot voting is where we stop and tell the truth. The prover detects the pattern and builds the harness, but it can’t assert the vote tally bit-precisely on a real governor that stores votes in opaque checkpoints — so it reports coverage-only instead of dressing up a tautology as a proof. All of this is validated on fixtures: evidence the harnesses work, not a claim that we’ve audited every protocol on chain.

A pass from the gate isn’t one check. It’s all of them, and any single failure flips the whole run to NO_SHIP:

• forge build and forge test both passed
• Slither came back clean, no critical finding
• The Solidity fake-success detector found nothing
• The reentrancy and access-control firewall has zero hard-block violations
• Halmos proved every check_* property — no violation, no unknown, at least one property actually checked

The most important line in the prover isn’t about proving. It’s about not lying when it can’t. If a binary is missing or a tool errors out before it reaches a verdict, that gate is marked degraded — “did not run” — and a degraded gate forces NO_SHIP. It is never counted as a pass.

A tool that did not run is not a tool that passed.

The symbolic step plays by the same rule. If Halmos returns unknown — a timeout, a path explosion — that is not a proof. It degrades. And where a property can’t be asserted bit-precisely (snapshot voting today), the gate emits a coverage-only check that says so out loud rather than a green it didn’t earn. Three things stay permanently outside the line, and we never imply otherwise:

• Your economic design. Incentives, peg stability, liquidation cascades — we simulate those under bounded scenarios and report them as tested, never proven.
• MEV in transaction ordering. Sandwiching and frontrunning across a block are properties of the market, not of one contract. We prove the contract-level defenses (slippage, deadline); we can’t prove the mempool.
• The oracle’s honesty. We prove your contract survives a lying price feed. We can’t prove the feed tells the truth.

Drawing that line is the credibility. A gate that claimed to catch everything would be the most dangerous thing on the chain.

A proof about source code that merely resembles what’s deployed is worth almost nothing. So the certificate is bound to keccak256(deployedBytecode) — the hash of the exact compiled runtime. The signed artifact says “these properties hold for thisbytecode,” and anyone can check that the contract on chain is byte-for-byte the one that was proven. Not a similar contract. That one.

That binding is what turns a proof into a certificate you can hand a counterparty, an auditor, or a regulator and have it mean something offline.

The web3 work runs through NZT-48, a special-ops persona over the base ISL agent. It adds no new machinery; it drives the substrate above — the contract-prover, the Foundry + Halmos + Slither harness, the ISL→Solidity codegen, the PR proof-gate. The voice is surgical: state the objective, make the move, show the solver output.

• Audit and prove foreign or pasted Solidity — find every contract and every candidate invariant, prove each with the real harness, fold the verdicts honestly, emit a signed bundle.
• Defensive exploit recon — map reentrancy, access control, overflow, price manipulation, unchecked external calls, upgrade traps. Each finding ships with a severity, a location, an exploit path, and a fix. Weaknesses get closed, never weaponized.
• Ship proven contracts from an ISL spec, and gate every .sol PR through the same bar.

Around it sits the operator surface — a scanner, MEV and mempool monitors, a wallet guard, attack simulation, a bytecode inspector, a deployer, a Time Machine for replaying state. Different tools, one goal: catch it before it’s immutable.

The discipline ported, and it got sharper on the way over. On the web we prove against a runtime; on-chain we prove against the input space itself and bind the result to the exact bytecode. The honesty rules came across unchanged, because they are the product: degraded is not a pass, unknown is not a proof, and a contract we can’t fully reason about is one we say so about.

Immutable code deserves more than “looks fine.” It deserves a proof bound to the bytecode, and an honest account of exactly what that proof covers and what it doesn’t.

More on the discipline behind it: Proof, not vibes and The pipeline is real.