Technical articles on programming languages, formal methods, and software verification
Embedding formal specification constructs directly into programming languages could revolutionize smart contract development and eradicate vulnerabilities in smart contracts.
Monolithic architectures create combinatorial explosions in verification complexity. Modular boundaries tame this growth, making bytecode-level formal verification tractable.
We compare UniswapX’s RFQ→exclusive-then-open Dutch two-stage auction with 1inch Fusion’s classic Dutch model to show how intent-based swaps curb MEV, failures, and liquidity fragmentation for better market-making.
Preparing Polkadot pallet Balances for formal verification by reimplementing it as an Ink! smart contract for isolated analysis.
An introduction to Fully Homomorphic Encryption (FHE), a cryptographic technique that allows computations to be performed on encrypted data without needing to decrypt it first.
A deep dive into implementing the 'tagless initial' pattern in Rust using enums and the never type to achieve zero-cost abstractions, demonstrated with optimized assembly output.
Exploring how game-theoretical modeling can be applied to decentralized exchange (DEX) protocols to identify design weaknesses and strategic attack vectors. We discuss the incentives and strategies of participants in Uniswap, SushiSwap, Cetus, and KyberSwap, illustrating how game theory can reveal exploits and inform more secure DEX design.
Demonstrating how to define a single-argument abstract Method trait in Rust, and use a PhantomData-based hint technique to automatically infer generic types.
A look into specialized C standard libraries like Newlib, picolibc, nanolib, and dietlibc, designed for resource-constrained environments where standard libraries like glibc are too large or complex.
In this post, we explore an advanced CPS (Continuation-Passing Style) implementation that leverages local memory pointers alongside arrow statements to declare an abstract program.