Smart Contract Design, Smart Contract Verification, and Smart Contract Formal Verification Best Practices

Summary: A 2026 field guide for decision‑makers: concrete design patterns, toolchains, and formal‑methods workflows that ship safer smart contracts faster—updated for Dencun-era EVM changes, modern Solidity compilers, and production-grade verification stacks across EVM and Move.

---

Why this matters now

Between March 2024’s Dencun upgrade and the rapid evolution of Solidity and verification tooling, several “old but gold” patterns are now footguns. For example, EIP‑6780 neutered SELFDESTRUCT for long‑lived contracts, breaking CREATE2-redeploy upgrade patterns; you should migrate to proxy or diamond architectures. EIP‑1153 added cheap transient storage for per‑transaction state (ideal for reentrancy locks), and MCOPY (EIP‑5656) changed the calculus for memory‑heavy code. Your design and verification plan needs to reflect these realities. (blog.ethereum.org)

---

Part I — Design best practices that age well in 2026

1) Architecture choices post‑Dencun

• Don’t rely on SELFDESTRUCT for “reset and redeploy at the same address.” Since March 13, 2024, SELFDESTRUCT no longer deletes code/storage for contracts created in previous transactions—it only transfers ETH. Upgrades must use standard proxies (Transparent, UUPS/1967) or a diamond (EIP‑2535). (blog.ethereum.org)
• Diamond pattern (EIP‑2535) is viable for large, modular systems. If you adopt it, enforce DiamondCut access control, ship a loupe facet, and adopt a consistent storage strategy (AppStorage or per‑facet diamond storage) to avoid storage collisions. (eips.ethereum.org)

Practical guardrails:

• Emit and monitor DiamondCut events; restrict upgrades to governance windows if your product/governance model allows. (arachnid.github.io)
• Document your storage strategy (e.g., AppStorage at slot 0) and commit to an order‑only append policy for all state structs. (safe-edges.medium.com)

2) Leverage new EVM features for security and gas

• Transient storage (EIP‑1153): Use TSTORE/TLOAD for reentrancy locks and per‑tx allowances; they clear at tx end and avoid storage refunds complexity. Solidity 0.8.28 added direct support for transient state variables of value types—budget for this in your 0.8.28+ migrations. (eips.ethereum.org)
• MCOPY (EIP‑5656): Replace manual memory copy loops and identity-precompile roundtrips with MCOPY for big memory moves (encoding/decoding, ABI packing). (eips.ethereum.org)
• PUSH0 (EIP‑3855): Compiler backends exploit it for smaller bytecode and lower gas; prefer modern compilers that target Cancun or newer. (eips.ethereum.org)
• Beacon block root in EVM (EIP‑4788): If you build trust‑minimized bridges, staking products, or restaking logic, you can reference beacon roots via the on‑chain contract to verify consensus state with Merkle proofs. Plan data structures and verification costs accordingly. (eips.ethereum.org)

3) Compiler, EVM versioning, and project defaults

• Pin compiler and EVM version in CI. Since 0.8.25, the default EVM is “cancun”; 0.8.26 adds require(bool, Error) for custom errors via IR; 0.8.28 unlocks transient storage variables; 0.8.29 brings experimental EOF (Osaka) backend and SMTChecker improvements. Use via‑IR and upgrade solc intentionally. (soliditylang.org)
• Storage layout discipline: generate and diff storageLayout on every PR before any upgrade. Foundry’s forge inspect storageLayout and solc’s JSON output let you gate merges. (learnblockchain.cn)

Recommended foundry.toml profile snippet:

[profile.default]
evm_version = "cancun"
via_ir = true
ast = true
build_info = true
extra_output = ["storageLayout"]
ffi = true  # needed by some upgrade validators

(learnblockchain.cn)

4) Upgradeability patterns with safety rails

• Prefer UUPS proxies for leaner deployments; use OZ Upgrades validations and storage layout checks in CI. For diamonds, enforce strict cut permissions and publish loupe interfaces. (docs.openzeppelin.com)
• Run Slither upgradeability checks early; they detect ID collisions, initializer misuse, and layout drift across versions. (github.com)

5) Operational controls built‑in

• Implement pause/guardian roles with strict scope; prove “pause halts dangerous flows but allows emergency withdrawals” using specs (see Part III).
• Plan monitoring at launch. OpenZeppelin Defender is being sunset (new signups disabled June 30, 2025; shutdown July 1, 2026). Migrate to the open‑source Monitor/Relayer or alternatives, and wire to Forta alerts. (blog.openzeppelin.com)

---

Part II — Verification you can ship: static + dynamic + runtime specs

The goal isn’t “run all tools”—it’s “prove the properties that matter for your protocol’s business logic,” and automate that proof in CI.

1) Static analysis, first

• Slither baseline: Run on pre‑commit with a curated allowlist. Include slither-check-upgradeability for proxies and diamonds. (github.com)
• Mythril for symbolic exploration of EVM bytecode (especially where inline assembly or hand‑rolled Yul exist). Use Docker for repeatability. (github.com)

2) Fuzzing and invariants that simulate mainnet chaos

• Foundry invariants: Raise depth beyond defaults for stateful systems; define explicit target selectors to cover risky sequences; enable call_override to probe reentrancy surfaces. Key settings include runs, depth, fail_on_revert, dictionary_weight, include_storage. (learnblockchain.cn)
• Coverage: Use forge coverage, but know its caveats—assembly lines and forked tests may underreport; keep a stable Foundry version in CI and avoid nightly regressions. (github.com)
• Echidna: Add property-based fuzzing for protocol invariants that need long random sequences and shrinking. Drop it in CI via the official GitHub action. (github.com)

Example Echidna property:

/// @notice total supply equals sum of balances
function echidna_supply_invariant() public view returns (bool) {
    return token.totalSupply() == sumBalances();
}

(github.com)

3) Runtime specification checks with Scribble

Annotate Solidity with invariants/postconditions that can be checked during fuzzing and tests. This front‑loads spec writing and increases signal for auditors. (diligence.consensys.io)

Example Scribble annotations:

/// invariant totalSupply() == __sum(balances);
/// if_succeeds {:msg "onlyOwner"} msg.sender == owner();
function mint(address to, uint256 amount) external { ... }

(diligence.consensys.io)

4) Solidity SMTChecker in CI

Enable the model checker to prove simple safety properties over unbounded inputs and transaction sequences, especially arithmetic, bounds, and some reentrancy patterns. Start with assertions/assumes and extend incrementally. (docs.solidity.org)

Example CI step (solc >= 0.8.29 suggested):

solc --model-checker-engine chc \
     --model-checker-targets assert,overflow,outOfBounds,balance \
     --model-checker-timeout 600 \
     --via-ir --evm-version cancun \
     --standard-json < compile.json

(soliditylang.org)

---

Part III — Formal verification that moves the needle

When the contract manages critical value (asset custody, liquidations, governance), elevate to formal verification that proofs hold across all states and sequences.

1) Certora Prover (EVM)

• Write CVL rules for safety properties and parametric rules to quantify over all public methods. As of CLI v5.0, parametric rules apply by default across contracts, increasing coverage. Recent 8.5.1 updates add Sui support and spec ergonomics. (docs.certora.com)

Example CVL rule (supply conservation):

rule totalSupply_is_sum_of_balances(env e) {
  require e.msg.sender != address(0);
  mathint sum = 0;
  forall (address a) { sum += token.balanceOf(a); }
  assert token.totalSupply() == sum;
}

(docs.certora.com)

Tips that avoid false confidence:

• Use multi_assert_check to isolate counterexamples per assertion. (docs.certora.com)
• Model external dependencies explicitly (e.g., underlying ERC‑20 that can change balances independent of your contract). v5 parametric coverage helps catch cross‑contract violations. (docs.certora.com)

2) Move Prover (Aptos/Sui)

For non‑EVM targets, Move’s spec language (MSL) and prover deliver exhaustive proofs on modules. Use struct invariants, function invariants, and global invariants for asset conservation and access control. (aptos.dev)

Example MSL invariant:

spec module MyToken {
  invariant forall a: address where exists<Coin>(a): global<Coin>(a).value >= 0;
}

(aptos.dev)

3) What to prove, concretely

• Asset accounting: totalSupply == sum(balances); no unauthorized mint/burn.
• Withdrawal/repayment math: rounding and fee paths; MCOPY‑based encoders behave identically to reference. (eips.ethereum.org)
• Invariant liveness under pause: pause blocks mints/transfers, but emergencyWithdraw always succeeds.
• Upgrade safety: storage layout preservation; initializer callable exactly once; no function ID collisions. (github.com)

---

Part IV — Monitoring, response, and lifecycle security

• Alerts: Subscribe to Forta bots (general or premium feeds) for governance, access control, suspicious activity, and financial anomalies. Integrate via Slack/Telegram/Webhooks or consume the GraphQL API. Stake if publishing your own bots. (docs.forta.network)
• Platform shift: With Defender sunsetting in 2026, plan migrations to OpenZeppelin’s open‑source Monitor/Relayer or your own infra. Track migration guides and timelines in your runbooks. (blog.openzeppelin.com)
• Incident drills: Write, rehearse, and monitor diamondCut/proxy upgrade windows; pre‑stage pause guardians; test “break‑glass” transactions on forks before mainnet.

---

Part V — Concrete examples and checklists

A) Transient storage reentrancy lock (Solidity ≥ 0.8.28)

// Pseudocode: use transient storage to auto-clear at tx end
contract Vault {
    transient bool locked; // 0.8.28+

    modifier nonReentrant() {
        require(!locked, "reentrant");
        locked = true;
        _;
        // no manual clear needed; resets at end-of-tx per EIP-1153
    }
}

(eips.ethereum.org)

B) Foundry invariant campaign hardening

[profile.default]
# raise exploration for stateful protocols
[invariant]
runs = 10_000
depth = 50
fail_on_revert = true
call_override = true
dictionary_weight = 90

(getfoundry.sh)

C) Slither and upgrade checks in CI

slither . --exclude-informational
slither-check-upgradeability . ProxyName --proxy-filename ./contracts --proxy-name TransparentUpgradeableProxy

(github.com)

D) Echidna in GitHub Actions

- uses: crytic/echidna-action@v2
  with:
    files: src/
    contract: Invariants
    config: echidna.yaml
    format: json

(github.com)

E) Storage layout diff gate

• Run forge inspect <Contract> storageLayout on both old and new impls; diff must be append‑only. Automate with OZ Upgrades Foundry plugin validations. (learnblockchain.cn)

---

Common 2026 pitfalls you can avoid

• Depending on SELFDESTRUCT for upgrades or ETH‑burn patterns: broken by EIP‑6780—migrate to proxies/diamonds. (eips.ethereum.org)
• Under‑using transient storage: reentrancy locks or per‑tx allowances still using SSTORE/SLOAD; switch to TSTORE/TLOAD for lower gas and fewer refunds gotchas. (eips.ethereum.org)
• Missing Dencun behavior in assumptions: blob gas (EIP‑4844) changes L2 cost models; don’t hardcode fee assumptions in on‑chain accounting. Track blobbasefee via EIP‑7516 if relevant to your protocol. (eips.ethereum.org)
• Ignoring compiler evolution: 0.8.26 custom‑error require, 0.8.28 transient vars, 0.8.29 experimental EOF—pin versions, test, and upgrade intentionally. (soliditylang.org)
• Relying on hosted Defender long‑term: schedule migration now; use open‑source Monitor/Relayer or alternatives before July 1, 2026. (blog.openzeppelin.com)

---

Executive roll‑out plan (what to ask your team for next sprint)

• Architecture decision record: Proxy vs Diamond, with storage strategy, upgrade governance window, and monitoring endpoints. (eips.ethereum.org)
• Tooling baseline in CI: Slither (+upgradeability), Foundry tests + invariants with coverage, Echidna properties for top‑3 invariants, SMTChecker job, and storageLayout diff gates. (github.com)
• Formal spec backlog: 5–10 CVL rules for your core value flows; parametric rules enabled; nightly runs on forks. (docs.certora.com)
• Monitoring & response: Forta subscriptions for governance/ACL/suspicious activity; OpenZeppelin Monitor migration playbook; pause/guardian drills on forks. (docs.forta.network)

---

Closing note

Design, verification, and formal methods should be continuous, not staged. Dencun‑era EVM changes and modern compilers give you new building blocks—use them deliberately, and pair them with invariant‑driven tests and machine‑checked specs. The outcome is not just fewer incidents; it’s faster shipping with higher confidence.

7Block Labs can help you prioritize the right properties, write specs that matter, and implement a CI pipeline that proves them on every change.