Type-safe EVM interaction for Elm. The runtime-exception guarantee extends past the wallet boundary.
See it, don't take our word: what is actually proved — the verification story: state-machine diagrams, the coverage ledger, and the CI that enforces it · live UI gallery — every primitive of the companion elm-web3-ui package, driven by these state machines with zero JS · coverage ledger · spec↔code conformance audit · EVM API coverage
Wraps window.ethereum, signs and sends transactions, decodes ABI, watches events — all behind explicit state machines and opaque types. Errors arrive as typed Msg values, not uncaught exceptions. No any, no stringly-typed addresses, no Promises swallowed at the boundary.
Most DeFi exploits hit the frontend, not the contracts. The JS dapp stack maximises that surface. This lib collapses it.
- Next to no JavaScript. App compiles to one small ES5 artifact. Runtime is ~20 KB.
- No React. No reconciler, no JSX-as-string, no
dangerouslySetInnerHTML. - No Next.js, no Vite, no Webpack. No middleware, no SSR proxy, no plugin chain.
- No npm dependency tree. Elm packages are curated; transitive supply-chain attacks have nowhere to land.
- No
eval, no template-string code execution. Elm has neither primitive. - Reproducible builds. Same input → byte-identical output. Audit the bundle, ship the bundle.
- No mutable globals. No
windowprototype-pollution surface.
- Addresses are opaque. You cannot construct an invalid address. Compiler refuses.
- BigInt is opaque. You cannot do float math on wei. Compiler refuses.
- Chain IDs are tagged. You cannot mix mainnet and testnet. Compiler refuses.
- No
any, no casts, no escape hatches. Anywhere. - Signatures carry their EIP type. EIP-191, EIP-712, raw — never confused.
- Decoders fail typed. Malformed RPC → typed
Msg, never a crash.
- Wallet state is a union. Disconnected, Connecting, Connected, WrongChain — handled or it doesn't compile.
- Transaction state is a union. Idle, Pending, Confirmed, Failed — handled or it doesn't compile.
- Signature state is a union. Same discipline.
- Cannot send a tx from a disconnected wallet. Compile error, not runtime undefined.
- Cannot read a balance from the wrong chain. Compile error, not stale UI.
- Pure functions. No mocks needed in tests.
- Total view functions. No "what if this prop is undefined" branch.
- Single compiled artifact. What you audit is what you ship.
- No async/await footguns. Cmds are explicit, traced through
update.
- Phishing-UI address swaps depend on string-typed addresses. Ours aren't strings.
- Fake-balance overlays depend on mutable view state. Ours isn't mutable.
- Wallet-bridge spoofs depend on prototype pollution. There's no prototype chain to pollute.
- The frontend deserves the same rigour as the contracts. This is what that looks like.
elm install intrepidshape/elm-web3Copy js/elm-web3-ports.js into your project and wire it up after your compiled Elm bundle:
<script src="elm.js"></script>
<script src="elm-web3-ports.js"></script>
<script>
var app = Elm.Main.init({ node: document.getElementById('app') });
setupPorts(app);
</script>Declare two ports in your Elm app:
port module Ports exposing (..)
import Json.Encode as E
import Json.Decode as D
port web3Cmd : E.Value -> Cmd msg
port web3Sub : (D.Value -> msg) -> Sub msgThe package communicates with the browser over two ports — one outgoing (web3Cmd) and one incoming (web3Sub). Everything in the JS bridge is wrapped in try/catch so errors arrive as typed Msg values rather than uncaught exceptions.
State machines are central to the design. Wallet.State, Transaction.Status, and Sign.SignState are all explicit union types — the compiler will tell you if you forget a branch.
The JS bridge has no npm dependencies. It calls window.ethereum.request() directly.
Opaque types for the primitives that appear everywhere:
address : String -> Maybe Address -- "0x" + 40 hex chars
txHash : String -> Maybe TxHash -- "0x" + 64 hex chars
chainId : Int -> ChainId
addressToString : Address -> String
txHashToString : TxHash -> String
chainIdToInt : ChainId -> IntPassing a TxHash where an Address is expected is a compile error.
Wallet state as an explicit state machine:
type State
= Disconnected
| ReadOnly -- rpcUrl set, no wallet
| Connecting
| Connected { address : Address, chainId : ChainId }
| WrongChain { address : Address, chainId : ChainId } ChainId
| Error StringstartConnect : State -> State
update : ChainId -> Msg -> State -> State
connect, disconnect : WalletCmd
switchChain : ChainId -> WalletCmd
selectWallet : String -> WalletCmd -- EIP-6963 RDNS
addChain : ChainConfig -> WalletCmd -- EIP-3085
watchAsset : { address, symbol, decimals, image } -> WalletCmd -- EIP-747
requestPermissions, getPermissions : WalletCmd -- EIP-2255
encode : WalletCmd -> E.Value
decoder : D.Decoder MsgA minimal wallet flow:
type alias Model =
{ wallet : Wallet.State
, providers : List Wallet.WalletProvider
}
type Msg
= ConnectWallet
| PickWallet String
| Web3Msg D.Value
expectedChain : T.ChainId
expectedChain =
Chain.chainId Chain.pulsechain
update msg model =
case msg of
ConnectWallet ->
( { model | wallet = Wallet.startConnect model.wallet }
, Ports.web3Cmd (Wallet.encode Wallet.connect)
)
PickWallet rdns ->
( model
, Ports.web3Cmd (Wallet.encode (Wallet.selectWallet rdns))
)
Web3Msg raw ->
case D.decodeValue Wallet.decoder raw of
Ok walletMsg ->
let
newWallet =
Wallet.update expectedChain walletMsg model.wallet
providers =
case walletMsg of
Wallet.WalletsDiscovered ps -> ps
_ -> model.providers
in
( { model | wallet = newWallet, providers = providers }
, Cmd.none
)
Err _ ->
( model, Cmd.none )
view model =
case model.wallet of
Wallet.Disconnected ->
button [ onClick ConnectWallet ] [ text "Connect" ]
Wallet.Connecting ->
text "Connecting…"
Wallet.Connected info ->
text (T.addressToString info.address)
Wallet.WrongChain _ expected ->
button [ onClick (PickWallet "") ] [ text "Switch network" ]
Wallet.ReadOnly ->
text "Read-only"
Wallet.Error err ->
text ("Error: " ++ err)Transaction lifecycle:
type Status
= Idle
| AwaitingSignature
| Submitted TxHash
| Confirming TxHash Int -- confirmation count
| Confirmed Receipt
| Failed String -- includes decoded revert reason when available
| Rejectedupdate : Msg -> Status -> Status
isPending : Status -> Bool
isTerminal : Status -> Bool
encodeCmd : TxCmd -> E.Value -- encode RequestReceipt for port
decoder : D.Decoder Msg
parseReceiptEvents : List (EventLog -> Maybe a) -> Receipt -> List aSending a transaction:
import Web3.Contract.Send as Send
import Web3.Transaction as Tx
type Msg
= Submit
| TxMsg D.Value
update msg model =
case msg of
Submit ->
( { model | tx = Tx.AwaitingSignature }
, Ports.web3Cmd
(Send.encode
(Send.payableCall
{ contract = routerAddress
, method = "buy(uint256)"
, args = [ Encode.uint256 minOut ]
, value = weiAmount
}
)
)
)
TxMsg raw ->
case D.decodeValue Tx.decoder raw of
Ok txMsg ->
( { model | tx = Tx.update txMsg model.tx }, Cmd.none )
Err _ ->
( model, Cmd.none )
viewTx status =
case status of
Tx.Idle -> text ""
Tx.AwaitingSignature -> text "Sign in your wallet…"
Tx.Submitted h -> text ("Pending: " ++ T.txHashToString h)
Tx.Confirming h n -> text (String.fromInt n ++ " confirmations")
Tx.Confirmed _ -> text "Confirmed"
Tx.Failed err -> text ("Failed: " ++ err)
Tx.Rejected -> text "Rejected"Read-only contract calls (eth_call):
readCall :
{ contract : Address
, method : String
, args : List E.Value
, decoder : D.Decoder a
, id : String
}
-> ReadCall a
withBlock : BlockNumber -> ReadCall a -> ReadCall a
withFrom : Address -> ReadCall a -> ReadCall a
encode : ReadCall a -> E.Value
responseDecoder : ReadCall a -> D.Decoder aWrite calls and deployments:
writeCall : { contract, method, args } -> WriteCall
payableCall : { contract, method, args, value : BigInt } -> WriteCall
withGasLimit : Int -> WriteCall -> WriteCall
encode : WriteCall -> E.Value
estimateGas : WriteCall -> E.Value
deployCall : { bytecode, args, gasLimit } -> E.Value
encodeRawSend : String -> E.ValueEvent subscriptions and log queries:
watchEvent : EventFilter -> E.Value
getLogs : GetLogsQuery -> E.Value
decoder : D.Decoder a -> D.Decoder (EventLog a)
logsDecoder : D.Decoder a -> D.Decoder (List (EventLog a))EventLog a carries data, contract, topics, blockNumber, txHash, and logIndex.
Batch multiple reads into one eth_call using the Multicall3 contract
(0xcA11bde05977b3631167028862bE2a173976CA11):
callSpec : Address -> String -> List E.Value -> CallSpec
batch : String -> List CallSpec -> MulticallRequest
encode : MulticallRequest -> E.Value
responseDecoder : List (D.Decoder a) -> D.Decoder (List (Result String a))EIP-712 typed data signing and EIP-191 personal signing:
typedData : { domain, types, primaryType, message } -> TypedData
encode : String -> Address -> TypedData -> E.Value
personalSign : String -> Address -> String -> E.Value
type SignState
= SignIdle
| SignPending String
| Signed String String
| SignFailed String String
| SignRejected String
startSign : String -> SignState -> SignState
signUpdate : SignMsg -> SignState -> SignState
isSignTerminal : SignState -> Bool
signatureDecoder : D.Decoder StringEIP-712 permit example:
permitRequest : T.Address -> T.Address -> BigInt -> Int -> Sign.TypedData
permitRequest owner spender value nonce =
Sign.typedData
{ domain =
{ name = Just "MyToken", version = Just "1"
, chainId = Just 369, verifyingContract = Just tokenAddress
, salt = Nothing
}
, types =
Dict.fromList
[ ( "Permit"
, [ { name = "owner", typeName = "address" }
, { name = "spender", typeName = "address" }
, { name = "value", typeName = "uint256" }
, { name = "nonce", typeName = "uint256" }
, { name = "deadline", typeName = "uint256" }
]
)
]
, primaryType = "Permit"
, message =
Json.Encode.object
[ ( "owner", Json.Encode.string (T.addressToString owner) )
, ( "spender", Json.Encode.string (T.addressToString spender) )
, ( "value", Json.Encode.string (BigInt.toString value) )
, ( "nonce", Json.Encode.int nonce )
, ( "deadline", Json.Encode.int 9999999999 )
]
}Native balance queries with correlation IDs:
getBalance : Address -> String -> Cmd
encode : Cmd -> E.Value
decoder : D.Decoder Msg -- GotBalance id weiBlock queries and polling:
getBlockNumber : String -> Cmd
getBlock : BlockNumber -> String -> Cmd
watchBlockNumber : String -> Cmd -- polls every ~4 seconds
getBlockTransactionCount : BlockNumber -> String -> Cmd
encode : Cmd -> E.Value
decoder : D.Decoder MsgGas price and EIP-1559 fee history:
getGasPrice : String -> Cmd
getFeeHistory : String -> Int -> Cmd
encode : Cmd -> E.Value
decoder : D.Decoder MsgMiscellaneous on-chain reads:
getTxCount : Address -> String -> Cmd
getStorageAt : Address -> Int -> String -> Cmd
getCode : Address -> String -> Cmd
getTransaction : TxHash -> String -> Cmd
encode : Cmd -> E.Value
decoder : D.Decoder MsgPure-Elm unit conversion, no port needed:
formatEther : BigInt -> String
parseEther : String -> Maybe BigInt
formatUnits : Int -> BigInt -> String
parseUnits : Int -> String -> Maybe BigIntChain definitions:
ethereum, sepolia : Chain
pulsechain, pulsechainTestnet : Chain
bsc, polygon, arbitrum, optimism, base : Chain
avalanche, zksync, fantom, gnosis, linea, scroll : Chain
custom : { chainId, name, rpcUrl, blockExplorer, nativeCurrency } -> Chain
chainId : Chain -> T.ChainId
name : Chain -> String
rpcUrl : Chain -> String
blockExplorer : Chain -> String| Chain | ID | Constructor |
|---|---|---|
| Ethereum | 1 | Chain.ethereum |
| Sepolia | 11155111 | Chain.sepolia |
| PulseChain | 369 | Chain.pulsechain |
| PulseChain Testnet | 943 | Chain.pulsechainTestnet |
| BNB Smart Chain | 56 | Chain.bsc |
| Polygon | 137 | Chain.polygon |
| Arbitrum One | 42161 | Chain.arbitrum |
| Optimism | 10 | Chain.optimism |
| Base | 8453 | Chain.base |
| Avalanche C-Chain | 43114 | Chain.avalanche |
| zkSync Era | 324 | Chain.zksync |
| Fantom | 250 | Chain.fantom |
| Gnosis | 100 | Chain.gnosis |
| Linea | 59144 | Chain.linea |
| Scroll | 534352 | Chain.scroll |
| Any EVM chain | custom | Chain.custom |
Arbitrary-precision integers for uint256 and int256 values. Base-10⁷ digit representation, no external dependencies.
fromInt : Int -> BigInt
fromString : String -> Maybe BigInt
fromIntString : String -> Maybe BigInt
fromHexString : String -> Maybe BigInt -- 0x-prefixed
toString : BigInt -> String
add, sub, mul : BigInt -> BigInt -> BigInt
div, mod : BigInt -> BigInt -> Maybe BigInt
compare : BigInt -> BigInt -> Order
gt, gte, lt, lte, eq : BigInt -> BigInt -> Bool
zero : BigInt
isZero : BigInt -> Bool
decoder : D.Decoder BigIntABI parameter helpers.
Encoders: address, uint256, int256, bool, string, bytes, bytes32, bytesN, list, tuple2, tuple3
Decoders: address, uint256, int256, bool, string, bytes32, uint8, uint16, uint32, uint64, uint128
Hex-slot decoders (for raw ABI hex without a JS ABI library):
hexSlot, uint256Slot, addressSlot, boolSlot, stringSlot, listSlot, tuple2Hex, tuple3Hex
Revert reason decoding:
decodeRevertReason : String -> Maybe StringKeccak256 via port:
keccak256 : String -> String -> Cmd
encode : Cmd -> E.Value
decoder : D.Decoder MsgGenerates typed Elm modules from Solidity ABI JSON:
bun codegen/generate.ts \
out/MyContract.sol/MyContract.json \
Generated.MyContract \
src/Generated/MyContract.elmEach ABI function becomes a typed encoder; each event becomes a typed decoder.
The proofs/ directory contains Lean 4 proofs and TLA+ specifications.
Lean 4 (all proofs close without sorry):
Address.lean— soundness, injectivity, and roundtrip foraddress/addressToStringTxHash.lean— same three properties fortxHashHexString.lean— same three properties forhexStringWalletCodec.lean— encode/decode roundtrip, injectivity, partial inverse, and tag separation forWalletCmdBigInt.lean— nine arithmetic theorems (normalize, add, multiply, shift, subtract, parse)AbiCodec.lean— bytes32 and address codec soundness, completeness, and roundtripRevertReason.lean— six theorems covering hex parsing, UTF-8 roundtrip, and selector/length guards
TLA+ model-checked:
WalletSpec.tla— wallet state invariants, no-deadlock livenessTransactionSpec.tla— terminal states stay terminal, confirmation count is monotonic
See proofs/COVERAGE.md for the full coverage map. All proofs use only core Lean 4 — no Mathlib.
cmditch/elm-ethereum— web3.js era, Task-based, no longer maintainedpurescript-web3— similar concept in PureScript
Intrepid Development — Solidity team. Dapps, contracts, audits.
We write the contracts and the frontends that talk to them. They deserve the same rigour. This lib is what we use on our own.
If you want it wired into a production frontend, or the dapp side hardened alongside a contract engagement: Jake@intrepiddev.com.au.
MIT © Intrepid Development