Language design improvements: fix Solidity's systemic flaws, inspired by Rust/Cairo/Move

[Th0rgal]

Goal

Go beyond Solidity feature parity (#1724) by fixing Solidity's well-documented systemic design flaws at the language level. Verity's unique position — a Lean-hosted EDSL that compiles to Yul with formal verification — means we can enforce safety invariants that Solidity leaves to programmer discipline, while keeping the migration path from Solidity straightforward.

This is the umbrella issue for language design improvements. The concrete work is tracked in axis sub-issues:

• Axis 1: Type system enrichment — newtypes, ADTs, pattern matching, Result types #1727 — Axis 1: Type System Enrichment: Semantic newtypes, ADTs + exhaustive pattern matching, Result types
• Axis 2: Compile-time safety enforcement — CEI, access control, unsafe blocks #1728 — Axis 2: Compile-Time Safety Enforcement: CEI enforcement with proof opt-out, @[requires Role] with auto-theorems, unsafe blocks
• Axis 3: Effect system and auto-theorem generation — @[view], @[modifies], @[no_external_calls] #1729 — Axis 3: Effect System & Auto-Theorem Generation: @[view]/@[modifies]/@[no_external_calls] verified annotations that generate frame condition theorems
• Axis 4: Storage safety — automatic EIP-7201 namespaced storage #1730 — Axis 4: Storage Safety: Automatic EIP-7201 namespaced storage

Design Philosophy

Easy to translate from Solidity, hard to introduce Solidity's bugs.

Every feature satisfies three constraints:

1. Translatable: A Solidity developer can look at the Verity equivalent and understand it immediately
2. Strictly safer: The Verity version prevents a class of bugs that Solidity allows
3. Formally leveraged: The safety property is provable or checkable at compile time through Lean's type system

How This Connects to #1724 (Solidity Parity)

The parity waves in #1724 provide the foundation. The axes here enrich those waves with safety guarantees that go beyond what Solidity offers:

#1724 Wave	Added from this issue
Wave 1: Type System (widths, enum)	+ Newtypes (types section), ADTs (inductive + match)
Wave 2: Control Flow & Safety (while/break/modifiers)	+ CEI enforcement, @[requires Role], effect annotations with auto-theorems
Wave 3: Storage (strings/bytes, structs, delete)	+ Automatic EIP-7201 namespaces
Wave 4: ABI & Memory (abi.encode, type introspection)	+ Call.Result type, externalCall! sugar
Wave 5: Composition (inheritance, interfaces)	+ unsafe blocks for delegatecall patterns

Retained Improvements (8 items)

1. Semantic Types (Newtypes) — Prevent Unit Confusion

Axis: Type System Enrichment | Inspired by: Rust, Haskell | Priority: P0

Everything in Solidity is uint256. Wei, token amounts, timestamps, slot indices are all the same type. This caused the Parity multisig freeze (~$280M) and countless DeFi exploits mixing up raw amounts vs. scaled amounts.

Decision: Requires a language-level change — a new types section in verity_contract. Cannot be done at contract level alone because ParamType is a closed inductive and valueTypeFromSyntax only recognizes fixed identifiers. The macro needs to be extended with ParamType.newtypeOf and the types block.

verity_contract MyToken where
  types
    Wei : Uint256
    Shares : Uint256

  storage
    totalAssets : Wei := slot 0
    totalShares : Shares := slot 1

  function deposit (assets : Wei) : Unit := do
    -- ERROR at compile time: can't add Wei + Shares
    let shares := Shares.wrap (Wei.unwrap assets)  -- explicit conversion required

Implementation: Lean newtypes are zero-cost wrappers. Compiled Yul uses raw uint256. Zero runtime overhead.

2. CEI Enforcement with Proof-Based Opt-Out — Prevent Reentrancy

Axis: Compile-Time Safety Enforcement | Inspired by: Cadence, Move | Priority: P0

Reentrancy remains the most iconic vulnerability class (DAO $60M, Rari Capital $80M, Orion Protocol $3M). Solidity relies on convention (CEI pattern) and opt-in library (ReentrancyGuard).

Decision: Hybrid approach with escalation ladder:

Opt-out path	Trust level	Mechanism
Provide a Lean proof of reentrancy safety	Zero trust	@[cei_safe by reentrancySafetyProof] — machine-checked
Use nonReentrant guard (already exists)	Low trust	Macro recognizes guard, relaxes CEI inside its body
Annotation	Explicit trust surface	@[allow_post_interaction_writes "reason"] — appears in --trust-report

Default: macro statically errors on any state write after an external call.

3. Role-Based Access Control with Auto-Generated Theorems

Axis: Compile-Time Safety Enforcement | Inspired by: Cadence, OpenZeppelin | Priority: P0

Access control is the #1 cause of smart contract losses ($953.2M cumulative). The key insight: @[requires Role] should auto-generate a theorem per enforced require.

@[requires Owner]
function setMinter (newMinter : Address) : Unit := do
  setStorageAddr minterSlot newMinter

Generates both:

1. Runtime: require (sender == getStorageAddr ownerSlot) "Not owner"
2. Theorem: theorem setMinter_requires_owner : ∀ s s' sender, setMinter_spec ... → sender = s.storage ownerSlot

Value: if someone removes the annotation, the theorem disappears and any downstream proof that depended on it breaks — compile-time failure.

4. ADTs + Exhaustive Pattern Matching

Axis: Type System Enrichment | Inspired by: Rust, Cairo, Lean | Priority: P1

Solidity has flat enums and no sum types. 51.4% of Solidity developers want algebraic datatypes; 34% want pattern matching (Developer Survey 2024).

Decision: Full design brainstormed. See #1727 for detailed compilation strategy including:

• Storage encoding as tagged unions (tag byte + max-width fields)
• New ParamType.adt, Expr.adtConstruct/adtTag/adtField, Stmt.matchAdt constructors
• Yul lowering via YulStmt.switch (already in Yul AST)
• Exhaustiveness checked by Lean's kernel for free
• ABI encoding as (uint8 tag, fields...) with max-width

5. Effect Annotations with Auto-Theorem Generation

Axis: Effect System | Inspired by: Rust | Priority: P1

@[view], @[modifies slots], @[no_external_calls] — verified by the macro AND auto-generate frame condition theorems. This is the bridge between the EDSL and the proof system.

Decision: Each annotation generates a specific theorem shape:

• @[view] → _is_view : ... → s'.storage = s.storage ∧ s'.events = s.events
• @[modifies balancesSlot, totalSupplySlot] → _frame : ... → ∀ slot, slot ≠ ... → s'.storage slot = s.storage slot
• @[no_external_calls] → _no_calls : ... → noExternalCallsInExecution s s'

These are exactly the frame conditions that make compositional verification scale, and they directly accelerate #1723.

6. Automatic EIP-7201 Namespaced Storage

Axis: Storage Safety | Inspired by: EIP-7201 | Priority: P1

Proxy storage collisions are a well-known attack vector. Verity already has explicit slots and conflict detection.

Decision: Option A — automatic from contract name. The macro computes keccak256("ContractName.storage.v1") as the base slot at elaboration time (Keccak already available in kernel). All slot assignments are offset from this base. Explicit slot N still works as an override.

7. Explicit unsafe Blocks

Axis: Compile-Time Safety Enforcement | Inspired by: Rust | Priority: P1

Maps to existing architecture: localObligations for trust-surface marking, --trust-report for machine-readable output, --deny-* flags for fail-closed verification.

unsafe "reason" do ... is syntactically mandatory for delegatecall, raw mstore to arbitrary offsets, raw sstore, inline Yul. The string description appears in --trust-report. Can be denied project-wide via --deny-unsafe.

8. Result Types for External Calls

Axis: Type System Enrichment | Inspired by: Rust, Cairo | Priority: P1

External calls return (bool, bytes) which developers routinely ignore. Implement alongside ADTs: Call.Result is a sum type with ! (bang) sugar for "revert on failure".

let result ← externalCall token "transfer(address,uint256)" [to, amount]
match result with
| .ok data => ...
| .err e => revert (formatError e)
-- Or shorthand:
externalCall! token "transfer(address,uint256)" [to, amount]

Items Explicitly Skipped

Item	Reason
Declarative invariants in contract surface	Already covered by existing spec/proof infrastructure
Bounded loops + gas awareness	Verity's forEach is already bounded; not a priority now
Checked arithmetic variants	safeAdd/safeSub/safeMul already exist; wrapping_*/saturating_* are nice-to-have
Immutable-by-default storage	Significant ergonomics change; revisit later

Migration Compatibility

All features are additive. Existing Solidity patterns translate directly:

Solidity Pattern	Verity Equivalent	Safety Improvement
uint256 amount	amount : Wei (newtype)	Prevents unit confusion
require(msg.sender == owner)	@[requires Owner]	Auto-generates access control theorem
modifier onlyOwner	@[requires Owner]	Generated, not manual
ReentrancyGuard	nonReentrant lock + CEI enforcement	Language-level, not library
view function	@[view] + auto-theorem	Machine-checked frame condition
(bool success, bytes data)	Call.Result + match	Un-ignorable error handling

Related Issues

• Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724 — Solidity feature parity (this issue extends Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724 with safety guarantees)
• Extend proven fragment to cover the full CompilationModel language surface #1723 — Proven fragment extension (Axis 3 directly accelerates this)
• Replace custom Yul semantics with EVMYulLean fork as compilation target #1722 — EVMYulLean migration (new features compile to Yul verified against EVMYulLean)
• [Compiler Enhancement] P2: Solidity interop profile for incremental migration #586 — Solidity interop support matrix

Sources

• Solidity Developer Survey 2024 Results
• Top 10 Smart Contract Vulnerabilities (Hacken, 2025)
• Smart Contract Languages: A Comparative Analysis (ScienceDirect, 2024)
• Move vs Solidity: Security in Smart Contracts
• Cadence: Language-Level Security (Flow)
• Vyper Design Principles