8b152a5a23
Adds formal verification DSL, multi-sig contract, and Hardhat plugin: synor-verifier crate: - Verification DSL for contract invariants and properties - SMT solver integration (Z3 backend optional) - Symbolic execution engine for path exploration - Automatic vulnerability detection (reentrancy, overflow, etc.) - 29 tests passing contracts/multi-sig: - M-of-N multi-signature wallet contract - Transaction proposals with timelock - Owner management (add/remove) - Emergency pause functionality - Native token and contract call support apps/hardhat-plugin (@synor/hardhat-plugin): - Network configuration for mainnet/testnet/devnet - Contract deployment with gas estimation - Contract verification on explorer - WASM compilation support - TypeScript type generation - Testing utilities (fork, impersonate, time manipulation) - Synor-specific RPC methods (quantum status, shard info, DAG)
43 lines
816 B
TOML
43 lines
816 B
TOML
[package]
|
|
name = "synor-verifier"
|
|
version = "0.1.0"
|
|
edition = "2021"
|
|
description = "Formal verification DSL for Synor smart contracts"
|
|
authors = ["Synor Team"]
|
|
license = "MIT"
|
|
repository = "https://github.com/synor/blockchain"
|
|
|
|
[dependencies]
|
|
synor-types = { path = "../synor-types" }
|
|
synor-crypto = { path = "../synor-crypto" }
|
|
|
|
# Serialization
|
|
serde = { version = "1.0", features = ["derive"] }
|
|
serde_json = "1.0"
|
|
|
|
# Parsing
|
|
pest = "2.7"
|
|
pest_derive = "2.7"
|
|
|
|
# SMT solver integration
|
|
z3 = { version = "0.12", features = ["static-link-z3"], optional = true }
|
|
|
|
# Symbolic execution
|
|
bitvec = "1.0"
|
|
|
|
# Error handling
|
|
thiserror = "1.0"
|
|
anyhow = "1.0"
|
|
|
|
# Logging
|
|
tracing = "0.1"
|
|
|
|
# Async
|
|
tokio = { version = "1.36", features = ["full"] }
|
|
|
|
[features]
|
|
default = []
|
|
z3-backend = ["z3"]
|
|
|
|
[dev-dependencies]
|
|
proptest = "1.4"
|