目录
- .githubfeat: v0.2.0 — 真实防重放/多签阈值校验、真实形式化证明、可运行示例与完整 CI12天前
- businessfeat: v0.2.0 — 真实防重放/多签阈值校验、真实形式化证明、可运行示例与完整 CI12天前
- examplesfeat: v0.2.0 — 真实防重放/多签阈值校验、真实形式化证明、可运行示例与完整 CI12天前
- prooffeat: v0.2.0 — 真实防重放/多签阈值校验、真实形式化证明、可运行示例与完整 CI12天前
- protocolfeat: v0.2.0 — 真实防重放/多签阈值校验、真实形式化证明、可运行示例与完整 CI12天前
- .gitignorefeat: real ECDSA secp256k1, 49 tests cover sig/fund/replay/bridge/contract/fee30天前
- LICENSEInitial commit2个月前
- README.mdfeat: v0.2.0 — 真实防重放/多签阈值校验、真实形式化证明、可运行示例与完整 CI12天前
- acceptance_review.mddocs: comprehensive README update reflecting full project structure and capabilities30天前
- moon.modfeat: v0.2.0 — 真实防重放/多签阈值校验、真实形式化证明、可运行示例与完整 CI12天前
- moon.pkgfeat(assert): complete default verifiers, fix tx dataflow, and link formal lemmas to runtime assertions2个月前
- pkg.generated.mbtifeat: real ECDSA secp256k1, 49 tests cover sig/fund/replay/bridge/contract/fee30天前
- proposal.mddocs: comprehensive README update reflecting full project structure and capabilities30天前
邀请码
版权所有：中国计算机学会技术支持：开源发展技术委员会
京ICP备13000930号-9
京公网安备 11010802047560号
CryptoAssert — Cryptocurrency Compliance & Security Assertion Library
Table of Contents
Overview
CryptoAssert eliminates the need for engineers to understand low-level cryptographic primitives when building cryptocurrency compliance checks. It provides a formally verified, type-safe abstraction over address validation, transaction verification, signature scheme compatibility, fee ratio enforcement, replay protection, contract safety, and cross-chain bridge security across 9 blockchain ecosystems and 5 signature schemes.
The library is organized in three layers, each with a distinct responsibility:
proof/transfer_proof.mbtpmoon prove, Why3 + Z3), executed for real in CIprotocol/business/fn[V: Trait]dispatchNotImplementedCore Capabilities
nonce/chain_idfield validation (consumed-nonce replay and cross-chain replay both rejected), plus EIP-155 style signature binding:chain_idandnonceare serialized into the signing message, so a signed transaction whose chain or nonce is tampered with fails ECDSA verificationmultisig_threshold-of-total_validators: zero / over-count / non-majority thresholds are rejected, sub-BFT thresholds warned), validator set size, amount boundaries, and chain ID validationmoon provevia Why3 + Z3, 14 goals proved; the CI prove job fails if any lemma cannot be provedsuberrorvariants with typed payloadsArchitecture
Project Structure
Line counts (implementation only):
protocol/e2e_verifier.mbtprotocol/ecdsa_secp256k1.mbtprotocol/simple_security_verifier.mbtproof/transfer_proof.mbtpprotocol/address_spec.mbtprotocol/uint256.mbtprotocol/bech32.mbtprotocol/eip712.mbtprotocol/transfer_runtime.mbtexamples/main.mbtprotocol/keccak256.mbtprotocol/rlp.mbtprotocol/smt.mbtprotocol/sha256.mbtprotocol/base58.mbtprotocol/transaction_spec.mbtprotocol/bigmath.mbtprotocol/security_spec.mbtprotocol/assert_result.mbtbusiness/security_assert.mbtbusiness/address_assert.mbtDesign Philosophy
1. Static Dispatch over Dynamic Dispatch
All traits use
self: Selfparameters andfn[V: Trait]generic syntax. This guarantees the compiler resolves every method call at compile time. There is no vtable lookup, nodyndispatch, and no runtimeNotImplementederror state.In a smart-contract context, a runtime “not implemented” branch is not a usability nuisance — it is a remote code execution vulnerability. By eliminating this class of errors entirely through the type system, CryptoAssert removes an entire attack surface.
2. Theorem-Proven Invariants
The
proof/transfer_proof.mbtpfile uses MoonBit’s first-class formal verification (.mbtpproof files in aproof-enabledpackage) to encode mathematical invariants about cryptocurrency transfers, replay protection, and bridge multisig quorums. Runningmoon provetranslates them to WhyML and hands each goal to the Why3 platform backed by the Z3 SMT solver — 14 goals, all mechanically proved. The CIprovejob runs this for real on every push and fails the build if any lemma cannot be proved.Having a machine-checked proof obligation wired into CI is a capability that mainstream blockchain ecosystems (Solidity, Rust/CosmWasm, Go/Cosmos SDK) do not offer natively.
3. Trait-Based Extension
The library ships with
DefaultVerifier,SimpleSecurityVerifier, andE2ETransactionVerifier, but users can implement their own verifiers by implementing theAddressVerifier,TransactionVerifier, andSecurityVerifiertraits. The compiler enforces completeness — missing any method is a compilation error, not a runtime panic.4. Structured Error Model
All errors use MoonBit’s
suberrormechanism (checked error subtypes). Each error variant carries structured payload data that enables programmatic error handling without string parsing. The 10 error variants cover the entire error space of cryptocurrency assertion failures.5. Separation of Proof and Runtime
The proof layer (
proof/transfer_proof.mbtp) defines mathematical theorems, while the runtime bridge (protocol/transfer_runtime.mbt) provides corresponding verification functions. Each runtime function references its corresponding lemma viaproof_requirein docstrings, creating a traceable link between formal verification and production code. Facts that the proof model cannot supply for free (see the modeling note in Layer 1) are enforced at runtime withBigIntchecks.Layer 1: Formal Proof Layer
File:
proof/transfer_proof.mbtp— a dedicated package enabled for proving viaproof/moon.pkg:This layer defines and proves mathematical theorems about cryptocurrency transfers, replay protection, and bridge multisig quorums using
moon prove, which translates the.mbtpfile to WhyML and invokes the Why3 verification platform backed by an SMT solver (Z3, CVC5, or Alt-Ergo).The CI
provejob executes exactly this and asserts1 of 1 packages proved/14 goals proved— a lemma that fails to prove fails the build. (Sanity-checked during development: adding a deliberately false lemma makesmoon proveexit non-zero.)Modeling Note (read this before trusting any proof)
MoonBit’s current proof prelude idealizes
UInt64as unbounded mathematical integers: the range fact0 ≤ x ≤ 2⁶⁴−1is not an implicit axiom. This file therefore follows two disciplines:proof_requirepremises — real input constraints, never the conclusion restated as a premise.BigIntchecks (check_fee_nonnegative_bigint,transfer_runtime.mbt,bigmath.mbt).The earlier
fee_nonnegative_lemma(⊢ fee ≥ 0with no premises) is unprovable under this model, and worse, it entered the axiom stack of subsequent goals and could make them vacuously “provable”. It has been removed; fee non-negativity is a runtimeBigIntcheck instead.Predicates
fund_conservation_inv(total_in, total_out, fee: UInt64)total_in ≡ total_out + feetransfer_state_invariant(pre_total, post_total: UInt64)pre_total ≡ post_totalLemmas & Theorems (14 goals, all proved)
All premises listed below are the actual
proof_requireclauses inproof/transfer_proof.mbtp.Fund conservation family
proof_require)proof_ensure)no_inflation_lemmafund_conservation_inv∧fee ≥ 0total_in ≥ total_outvalue_monotonic_lemmain1 ≥ in2∧ both ≥out + fee(in1 − out − fee) ≥ (in2 − out − fee)overflow_safe_lemmaa ≥ 0∧b ≥ 0∧a ≤ max − ba + b ≥ a∧a + b ≥ b∧a + b ≤ maxtransfer_correctness_theoremfund_conservation_inv∧fee ≥ 0Replay protection family (backs
check_replay_protection)nonce_replay_rejection_lemmaexpected == current + 1∧replayed ≤ currentreplayed ≠ expected— a consumed nonce can never pass the equality checkchain_id_binding_lemmaexpected_chain_id ≥ 1∧tx_chain_id == expected_chain_idtx_chain_id ≥ 1— a tx that passes the chain-ID check is never chain-unboundBridge multisig family (backs
check_bridge_security)multisig_quorum_intersection_lemmatotal ≥ 1∧threshold ≤ total∧3·threshold ≥ 2·total + 12·threshold ≥ total + 1∧threshold ≥ 1— any two BFT quorums intersect, so the bridge cannot sign two conflicting messagesUInt256 limb bounds & account model
model_balance_lemmalocked ≥ 0∧available ≥ 0∧total == locked + availabletotal ≥ locked∧total ≥ availableuint256_add_no_overflow_lemmacarry_in ≤ 1∧a3 ≤ (max−1) − b3uint256_sub_no_underflow_lemmaa3 > b3a3 ≥ b3uint256_mul_no_overflow_lemmacarry == 0a3·b3 ≥ 0∧a3·b3 ≤ maxProof ↔ runtime bridge family
bridge_soundness_lemmafund_conservation_inv∧ all values in[0, max]in == out + feelifts losslessly to BigIntbridge_conservation_lemmafund_conservation_inv∧fee ≥ 0∧out ≤ max − feein ≥ out∧in == out + feebigint_extended_conservation_lemmafund_conservation_inv∧fee ≥ 0∧out ≤ max − feein ≥ out∧in == out + feeEach lemma body contains explicit
proof_assertstatements that guide the SMT solver through the logical derivation. The proofs are verifiable by running:Why This Matters in Production
Without formal proof, a developer writes
assert(total_in == total_out + fee)and hopes it is correct. Here, the SMT solver checks each lemma for all values satisfying its stated premises — not for a finite sample of test inputs. The guarantee is exactly as strong as the premises are honest: range facts are stated explicitly (see the modeling note above), and the runtimeBigIntbridges enforce them on real data. Together this eliminates entire categories of bugs — inflation attacks, conservation violations, nonce-replay acceptance, and under-thresholded bridge multisigs — before code reaches production.Layer 2: Protocol Specification Layer
Directory:
protocol/The protocol layer defines what must be verified — the type contracts, trait interfaces, and the reference
DefaultVerifierimplementation.AddressVerifier Trait
All 9 address types supported by
DefaultVerifier:BtcP2pkh1BtcP2sh3BtcBech32bc1BtcBech32mbc1pEth0xEthEip550xSolanaTronTCosmoscosmos1TransactionVerifier Trait
SecurityVerifier Trait
Layer 2 (Extended): Cryptography Primitives
CryptoAssert includes production-grade implementations of core cryptographic primitives used across major blockchain ecosystems.
ECDSA secp256k1 —
protocol/ecdsa_secp256k1.mbt(443 lines)Full FIPS 186-4 ECDSA implementation over the secp256k1 curve:
y² = x³ + 7overF_pwith SEC 2 secp256k1 parametersBigIntfor arbitrary precisionSHA-256 —
protocol/sha256.mbt(169 lines)FIPS 180-4 compliant SHA-256 implementation with explicit 32-bit masking for cross-platform consistency (wasm32, wasm64, native targets). Includes
sha256d(double SHA-256, Bitcoin standard).Keccak-256 —
protocol/keccak256.mbt(193 lines)Keccak-256 implementation for Ethereum compatibility. Keccak-256 is not SHA3-256 — they differ in padding. This implementation uses:
keccak256_to_nibblesfor EIP-55 address checksummingkeccak256("")=c5d24601…,keccak256("abc")=4e03657a…) in the test suiteBase58 / Base58Check —
protocol/base58.mbt(161 lines)Bitcoin-compatible Base58 encoding with:
0,O,I,l)base58_check_verify— full Base58Check checksum validation (SHA-256d)base58_check_validate— address validation with version byte and payload length checksBech32 / Bech32m —
protocol/bech32.mbt(233 lines)BIP 173 and BIP 350 compliant Bech32/Bech32m implementation:
cosmos_verifyfor Cosmos/IBC ecosystem addressesEIP-712 —
protocol/eip712.mbt(229 lines)Ethereum EIP-712 typed structured data hashing:
compute_type_hash— keccak256(encodeType(def))encode_and_hash_struct— structHash = keccak256(typeHash || padded fields)compute_eip712_message_hash— messageHash = keccak256(\x19\x01 || domainHash || structHash)address,uint256,bytes32,string,boolparse_type_definitionwith bracket-aware field splittingRLP —
protocol/rlp.mbt(177 lines)Ethereum Yellow Paper Appendix B RLP decoder:
rlp_decode,rlp_as_string,rlp_as_listAPIbytes_to_hexhelper for RLP-to-hex conversionSparse Merkle Tree —
protocol/smt.mbt(171 lines)256-layer Sparse Merkle Tree verifier using Keccak-256:
SMTProofstruct with side nodes, bit mask, and valueverify_smt_inclusion— verify key/value exists under root hashverify_smt_exclusion— verify key does not exist in treeLayer 2 (Extended): E2E Production Verifier
File:
protocol/e2e_verifier.mbt(656 lines)The E2E production verifier provides a complete, production-ready transaction verification pipeline implementing the
TransactionVerifiertrait with real ECDSA secp256k1 operations.Transaction Signing & Verification
Fund Conservation
Replay Protection
Contract Safety Audit
Bridge Security Audit
Full Transaction Validation Pipeline
TransactionVerifier Trait Implementation
E2ETransactionVerifierimplements all 5TransactionVerifiermethods:validate_transactionverify_signaturecompute_txidestimate_feevalidate_token_transferLayer 2 (Extended): Lemma Runtime Bridge
File:
protocol/transfer_runtime.mbt(225 lines)The lemma runtime bridge maps each formal lemma from
proof/transfer_proof.mbtpto a runtime-callable verification function. Each function:proof_requireBigIntinternally for overflow-safe comparisonscheck_fund_conservationfund_conservation_invtotal_in == total_out + feecheck_overflow_safeoverflow_safe_lemmaa + b ≥ aanda + b ≥ bcheck_fee_nonnegativefee_nonnegative_lemmais unprovable under the idealized-integer model and was removed)fee ≥ 0(BigInt version)check_no_inflationno_inflation_lemmatotal_in ≥ total_outcheck_value_monotonicvalue_monotonic_lemmacheck_transfer_state_invarianttransfer_state_invariantpre_total == post_totalcheck_transfer_correctnesstransfer_correctness_theoremverify_transfer_balance_chaincheck_transfer_bigintLayer 2 (Extended): BigMath & UInt256
BigMath —
protocol/bigmath.mbt(96 lines)BigInt-based amount parsing and operations designed for Ethereum’s 18-decimal precision, where UInt64 overflows above ~18.44 ETH:
parse_bigint_amountbigint_fund_conservationtotal_in == total_out + feebigint_no_inflationtotal_in >= total_outafter conservation checkbigint_transfer_correctnesssum_bigint_amountsbigint_verify_transfer_balance_chainUInt256 —
protocol/uint256.mbt(325 lines)Full 256-bit unsigned integer implementation (4 × UInt64 limbs, little-endian):
from_uint64(UInt64) -> UInt256add(UInt256, UInt256) -> (UInt256, Bool)sub(UInt256, UInt256) -> (UInt256, Bool)mul(UInt256, UInt256) -> (UInt256, Bool)div_mod(UInt256, UInt256) -> (UInt256, UInt256)?to_string(UInt256) -> Stringfrom_string(String) -> UInt256?is_zero(UInt256) -> BoolLayer 2 (Extended): Additional Modules
SimpleSecurityVerifier —
protocol/simple_security_verifier.mbt(439 lines)A complete, production-ready
SecurityVerifierimplementation with BigInt-based numerical validation. Construct it with@protocol.SimpleSecurityVerifier::new().tx.chain_idvalidation (missing / zero / mismatch vsexpected_chain_id→Unsafe), realtx.noncevalidation (missing →Unsafe;< expected_nonce→Unsafereplay;> expected_nonce→Warninggap), locktime requirement, nonce-reuse warningmultisig_threshold-of-total_validators: zero / over-count / non-majority →Unsafe, sub-BFT ⌊2n/3⌋+1 →Warning, backed bymultisig_quorum_intersection_lemma), validator set size analysis, amount range consistency, address format validation, chain ID validationBigInt-based min/max boundary checks with structured resultsAll parse failures convert to
SecurityAssertResult::Unsafe— no panics at runtime.Layer 3: Business Assertion Layer
Directory:
business/The business layer provides how to verify — concrete assertion functions that consume trait implementations and return structured results or raise typed errors.
Address & Signature Assertions (
address_assert.mbt)assert_address_formatfn[V: AddressVerifier](V, String, AddressType) -> AssertionResult raise AssertErrorassert_sig_scheme_compatiblefn(SignatureScheme, AddressType) -> AssertionResult raise AssertErrorassert_tx_signaturefn[V: TransactionVerifier](V, TransactionSpec) -> AssertionResult raise AssertErrorSecurity Assertions (
security_assert.mbt)assert_transaction_balancefn(TransactionSpec) -> AssertionResult raise AssertErrorΣinputs ≡ Σoutputs + feeassert_replay_protectionfn[V: SecurityVerifier](V, TransactionSpec, ReplayProtectionSpec) -> AssertionResult raise AssertErrorassert_amount_in_rangefn[V: SecurityVerifier](V, String, String, String) -> AssertionResult raise AssertErrorassert_fee_within_ratiofn[V: SecurityVerifier](V, String, String, String) -> AssertionResult raise AssertErrorassert_contract_safetyfn[V: SecurityVerifier](V, TokenSafetySpec) -> AssertionResult raise AssertErrorassert_bridge_securityfn[V: SecurityVerifier](V, BridgeSpec) -> AssertionResult raise AssertErrorBalance Verification
The
assert_transaction_balancefunction directly corresponds to the formally provenfund_conservation_invpredicate (proof/transfer_proof.mbtp). It performs:a + b ≥ acheck at each addition.total_in ≡ total_out + feewith overflow check ontotal_out + fee.AmountImbalancewith exact values if conservation fails.This is the runtime embodiment of the compile-time-proven theorem.
Type System Reference
Enumerated Types
AddressType— 9 blockchain address formatsBtcP2pkhBtcP2shBtcBech32BtcBech32mEthEthEip55SolanaTronCosmosSignatureScheme— 5 cryptographic signature algorithmsEcdsaSecp256k1Ed25519Sr25519Bls12381SchnorrSecp256k1HashScheme— 6 hash algorithmsSha256Keccak256Blake2b256Blake2s256Ripemd160Sha256dChecksumType— 4 checksum strategiesNoneBase58CheckBech32Eip55TxStatus— 5 transaction lifecycle statesPending,Confirmed,Failed,Dropped,UnknownTxValidationCode— 9 transaction validation outcomesValid,InvalidSignature,InvalidInput,InvalidOutput,InsufficientFee,DoubleSpend,Expired,AmountMismatch,ChainIdMismatchSecurityAssertResult— 3-tier security verdictSafe,Warning(String),Unsafe(String)ContractSafetyMode— 5 smart contract safety controlsOwned,TimeLock,Pausable,Upgradeable,RateLimitedStruct Types
AddressLengthRangemin_chars: UInt,max_chars: UInt,byte_len: UIntAddressFormatSpecty, length, checksum_type, prefix_req, charset, descriptionPrecisionSpecdecimals: UInt,unit_vals: String,symbol: StringTxInputSpectxid, vout, script_sig, amount_strTxOutputSpecaddress, amount_str, script_pubkey, is_changeFeeSpecrate_str, total_str, unit_descTransactionSpecversion, inputs[], outputs[], locktime, fee, txid, nonce: UInt64?, chain_id: UInt?, sig_scheme, signature_hex?, public_key_hex?nonce/chain_idare serialized into the signing message and txidTokenTransferSpecfrom, to, contract, amount_str, chain_id, precisionSignatureVerifySpecmessage_hex, signature_hex, public_key_hex, schemeReplayProtectionSpecrequire_nonce, expected_nonce: UInt64?, require_chain_id, expected_chain_id: UInt, require_timestamp, max_nonce_reuseTokenSafetySpechas_mint, mint_controlled, has_burn, has_pause, safety_modes[]BridgeSpeccontract_address, target_chain_id, min_amount_str, max_amount_str, has_validator_set, min_validators, multisig_threshold, total_validatorsSMTProofside_nodes: Array[Bytes], bit_mask: FixedArray[Bool], value: BytesEip712Fieldname: String, ty: StringEip712TypeDefinitionname: String, fields: Array[Eip712Field]UInt256v0, v1, v2, v3: UInt64RlpItemString(Bytes)orList(Array[RlpItem])ECPointx: BigInt, y: BigIntTrait Reference
AddressVerifieraddress_format_spec(self, AddressType)AddressFormatSpecvalid_address_length_range(self, AddressType)AddressLengthRangevalidate_checksum(self, AddressType, String)Booladdress_precision(self, SignatureScheme)PrecisionSpechash_output_length(self, HashScheme)UIntis_valid_hash_size(self, Bytes, HashScheme)BoolTransactionVerifiervalidate_transaction(self, TransactionSpec)TxValidationCodeverify_signature(self, SignatureVerifySpec)Boolcompute_txid(self, TransactionSpec)Stringestimate_fee(self, TransactionSpec, String)FeeSpecvalidate_token_transfer(self, TokenTransferSpec)TxValidationCodeSecurityVerifiercheck_replay_protection(self, TransactionSpec, ReplayProtectionSpec)SecurityAssertResultcheck_contract_safety(self, TokenSafetySpec)SecurityAssertResultcheck_bridge_security(self, BridgeSpec)SecurityAssertResultvalidate_amount_range(self, String, String, String)SecurityAssertResultcheck_fee_ratio(self, String, String, String)SecurityAssertResultError Model
All errors use MoonBit’s
suberrormechanism — checked error subtypes that the compiler enforces at call sites. Each variant carries domain-specific payload data.suberror AssertError— 10 variantsInvalidPrefix(String, String)— address, expected prefixInvalidLength(String, UInt, UInt)— address, min, maxInvalidCharacter(String, Char)— address, illegal charChecksumMismatch(String)— addressAmountImbalance(String, String, String)— total_in, total_out, feeIncompatibleScheme(SignatureScheme, AddressType)SignatureVerificationFailed(String)— txidNumericParseError(String)— parse detailHashLengthMismatch(UInt, UInt)— actual, expectedSecurityCheckFailed(String)— reasonHandling Errors
Quick Start
Prerequisites
moon prove; setWHY3DATA/WHY3LIBfromwhy3 --print-datadir/why3 --print-libdir, optionallyZ3PATH)Run the Examples
Every snippet below is excerpted from the runnable example program in
examples/main.mbt, which CI compiles and runs on every push (asserting on its output), so the documentation can never drift from the published API again:Adding CryptoAssert to Your Project
Or add to
moon.modmanually:Then in your
moon.pkg:Example 1: Address Format Validation
Example 2: Signature Scheme Compatibility (Pure Function)
Example 3: E2E Production Transaction Pipeline
Example 4: ECDSA Signature Generation & Verification
Example 5: Replay Protection — Real nonce / chain ID Checks
Example 6: Bridge Multisig Audit
Example 7: BigInt Fund Conservation (Production Recommended)
Example 8: Sparse Merkle Tree Verification
API Reference
The sections above (Type System Reference, Trait Reference, and Layer 3: Business Assertion Layer) constitute the complete API catalog for this library. For an interactive HTML API reference with cross-linked types and search, run:
This generates browsable documentation in the
_build/doc/directory.Extending the Library
Implementing a Custom
AddressVerifierTo add support for a new blockchain (e.g., Polkadot), implement all 6 methods of the
AddressVerifiertrait:The compiler will not compile if any method is missing. This is enforced statically — no runtime
NotImplementederror can ever occur.Adding New Chain Support
The recommended workflow:
AddressVerifierfor your chain’s address format.TransactionVerifierfor your chain’s transaction structure.SecurityVerifierfor your chain’s security model.business/business_test.mbtfor patterns).transfer_proof.mbtpwith chain-specific invariants and prove them withmoon prove.Testing & Quality Assurance
Test Coverage
protocol/spec_easy_test.mbtprotocol/spec_difficult_test.mbtbusiness/business_test.mbtTest Execution Summary
moon test --target nativeandmoon test --target wasm-gcmoon check --deny-warnpasses with zero warningsQuickCheck Property Bombardment
The business test suite uses
moonbitlang/quickcheck@0.14.0to systematically verify properties through randomized input generation:IncompatibleSchemecarries correct(scheme, addr)Total: 9,100+ property check rounds across the full 5×9 compatibility matrix.
Test Execution
Security Considerations
Compile-Time Guarantees
Zero
NotImplemented: All traits useself: Selfwithfn[V: Trait]syntax. The compiler rejects any incomplete trait implementation at compile time. This eliminates a class of vulnerabilities where runtime “not implemented” branches could be exploited in smart contract contexts.Overflow Protection: The
overflow_safe_lemmais proven by Z3 (under its explicit non-negativity and bound premises — see the Layer 1 modeling note) and enforced at runtime in bridging functions. Every accumulation is guarded by overflow checks.Fund Conservation: The conservation lemmas are verified by the SMT solver for all values satisfying their stated
proof_requirepremises. Both UInt64 and BigInt runtime implementations are provided; the BigInt path enforces the range premises on real data.Numeric Domain: UInt64 vs BigInt
The current formal proofs operate on
UInt64(max ≈ 1.84 × 10¹⁹), which is sufficient for Bitcoin (Satoshi), Solana (Lamport), and most UTXO-based chains where individual UTXO values fit within 64 bits.For Ethereum and EVM-compatible chains that use 256-bit integers, the library provides:
bigmath.mbt: BigInt-based amount operations (no overflow limit)uint256.mbt: Full 256-bit unsigned integer (add/sub/mul/div)check_transfer_bigint: Production-recommended BigInt verificationSupported Cryptographic Primitives
Attack Surface Analysis
overflow_safe_lemma+ Z3 + runtime guardfund_conservation_inv+ Z3InvalidPrefixerrorInvalidCharactererrorChecksumMismatcherrorIncompatibleSchemeerrorTxValidationCode::DoubleSpendtx.noncevsexpected_noncecheck +nonce_replay_rejection_lemmatx.chain_idvsexpected_chain_idcheck + EIP-155 style signature bindingmultisig_threshold-of-total_validatorsverification (majority + BFT) +min_validatorscheckProduction Hardening Recommendations
Use BigInt for high-value transfers — Prefer
check_transfer_bigintover UInt64-based functions for Ethereum and EVM-compatible chains.Use a secure random number generator — The QuickCheck LCG in tests is deterministic by design. Production key generation should use OS-provided CSPRNGs.
Add chain-specific invariants — Extend
proof/transfer_proof.mbtpwith chain-specific theorems (e.g., staking conservation, slashing invariants).Audit custom verifiers — While the trait system guarantees completeness, the semantic correctness of custom
SecurityVerifierimplementations is the integrator’s responsibility.Build, Prove & Test
Development Commands
CI/CD
The project uses GitHub Actions for continuous integration:
CI Pipeline (
.github/workflows/ci.yml) — 4 jobs, all realcheckmoon check --deny-warn+moon fmt && git diff --exit-codebuildmoon build+moon run examples --target native, then greps the output for key results (signature valid: true,replayed old nonce → Unsafe,7-of-9 (BFT quorum) → Safe, …)testmoon test -v --target native+moon test --target wasm-gcproveWHY3DATA/WHY3LIB/Z3PATH, runsmoon proveand asserts1 of 1 packages proved/14 goals provedPublished Package
Kali-Leo/moonbit-CryptoAssertv0.2.0Comparison with Industry Alternatives
moon prove(Why3/Z3)NotImplemented)Key differentiator: CryptoAssert ships proof-carrying code — mathematical theorems about fund conservation, replay protection, and bridge multisig quorums are verified by an SMT solver via
moon proveon every CI run, with the honest modeling premises documented alongside. It also provides the broadest suite of built-in cryptographic primitives (ECDSA, SHA-256, Keccak-256, Base58, Bech32, EIP-712, RLP, SMT) among multi-chain assertion libraries.Changelog
0.2.0 (2026-07-30)
Response to the OSC 2026 acceptance review — every finding addressed with code, proofs, and CI enforcement:
Core capability completion
TransactionSpecgainsnonce : UInt64?andchain_id : UInt?;ReplayProtectionSpecgainsexpected_nonce/expected_chain_id.check_replay_protectionnow validates the actual field values (missing/zero/mismatched chain ID →Unsafe; missing nonce →Unsafe; consumed nonce →Unsafe; nonce gap →Warning).chain_idandnonceare serialized into the signing message and txid, so signatures cryptographically bind chain and sequence number.BridgeSpecgainsmultisig_threshold/total_validators;check_bridge_securityrejects zero, over-count, and non-majority thresholds and warns below the BFT quorum ⌊2n/3⌋+1.Formal proofs actually execute
proof-enabledpackage (proof/);moon provetranslates them to WhyML and runs Why3 + Z3 for real — 14 goals proved, and a false lemma makes the build fail. The CIprovejob asserts the goal count.fee_nonnegative_lemmaremoved) and extended withnonce_replay_rejection_lemma,chain_id_binding_lemma, andmultisig_quorum_intersection_lemmabacking the new runtime checks.Cryptography fixes
0x,bc1,cosmos1), which mis-rejected all prefixed addresses.assert_tx_signaturecould never verify a transaction signed bysign_transaction).Docs, examples & CI
examples/package mirroring the README Quick Start; CI builds and runs it and asserts on its output.Breaking changes
TransactionSpec,ReplayProtectionSpec,BridgeSpecconstruction requires the new fields;verify_replay_protection,audit_bridge_security, andfull_tx_validation_pipelinehave new signatures (hence 0.2.0).License
Apache 2.0 License — see LICENSE
Contributing
proof/transfer_proof.mbtpwith chain-specific invariants and prove them.moon check --deny-warn && moon prove && moon test --target nativebefore submitting.Built with MoonBit · Proven with Why3/Z3 via
moon prove· Tested with QuickCheckMaking cryptocurrency compliance verification accessible, provably safe, and production-ready.