#formal-methodsView all tags

• PQC Research Series — Part 5

  September 29, 2026 · 23 min — #post-quantum-cryptography#formal-methods#side-channels#constant-time#cryptography#security-engineering#embedded#systems

• PQC Research Series — Part 4

  May 2, 2026 · 18 min — #post-quantum-cryptography#cryptography#formal-methods#reductions#concrete-security#lattices#fiat-shamir#QROM#security-engineering#embedded#systems

• PQC Research Series — Part 3

  April 30, 2026 · 19 min — #post-quantum-cryptography#cryptography#formal-methods#QROM#random-oracle-model#fiat-shamir#signatures#zero-knowledge#security-engineering#systems

• PQC Research Series — Part 2

  April 26, 2026 · 13 min — #post-quantum-cryptography#formal-methods#cryptography#lattices#LWE#SIS#reductions#security-engineering

• PQC Research Series — Part 1

  April 24, 2026 · 17 min — #post-quantum-cryptography#formal-methods#cryptography#systems#threat-modeling#QROM

• The KelpDAO Exploit Was Not a Bug

  April 19, 2026 · 22 min — #incident-analysis#security#DeFi#cross-chain#distributed-infrastructure#formal-methods#protocol-design#Ethereum#LayerZero

• Stateful Signatures Are a Distributed Systems Problem: XMSS/LMS Without Index Reuse

  April 1, 2026 · 10 min — #research-notes#post-quantum-cryptography#cryptography#security-critical-infrastructure#devsecops#iiot-platforms#distributed-systems#formal-methods

• Termination Is a Security Boundary: HotStuff Under UC, Delay Attacks, and the Uncomfortable Gap to Rust

  March 28, 2026 · 13 min — #research-notes#distributed-systems#consensus#BFT#formal-methods#cryptography#Rust#security

• Secure Distributed Storage: Erasure Coding Under Adversaries

  March 1, 2026 · 3 min — #research-notes#distributed-systems#cryptography#formal-methods#security

• Verifiable Computation as Infrastructure: Proof Systems at Scale

  February 1, 2026 · 3 min — #research-notes#distributed-systems#cryptography#formal-methods#security

• Composable Security: Where Proofs Break in Real Systems

  January 1, 2026 · 3 min — #research-notes#distributed-systems#cryptography#formal-methods#security

• Spec-Driven Development: Making the Spec the Center of Gravity

  December 1, 2020 · 4 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Designing APIs for Correctness: Types, Lifetimes, and Capabilities

  November 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Verified Crypto Interfaces: Constant-Time Boundaries and Misuse Resistance

  October 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Symbolic Execution: When Brute Force Becomes Logic

  September 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Concurrency Testing in Rust: Loom, Schedules, and Determinism

  August 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Fuzzing Protocol Parsers: When Inputs Are Adversarial

  July 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Differential Testing: Using Other Implementations as Oracles

  June 1, 2020 · 4 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Property-Based Testing: Finding Bugs You Didn’t Imagine

  May 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Refinement: Proving Your Implementation Matches the Spec

  April 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Model Checking at Scale: State Explosion and How to Cheat

  March 1, 2020 · 4 min — #research-notes#formal-methods#verification#protocol-design#correctness

• TLA+ for Engineers: Modeling the Minimal Thing That Can Break You

  February 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Safety/Liveness Catalog: A Practical Checklist for Protocol Specs

  January 1, 2020 · 3 min — #research-notes#formal-methods#verification#protocol-design#correctness

• Security vs Reliability: When the Same Bug Has Two Names

  December 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Reproducible Builds: Trusting Artifacts in a Hostile World

  November 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Observability as Specification: SLOs, Error Budgets, and Contracts

  October 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Fault Injection: Turning Unknown Unknowns into Test Cases

  September 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Memory Models and Concurrency: Reasoning About Races

  August 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Crash Consistency: Durable State Without Mysticism

  July 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Cryptographic Hygiene: Domain Separation, KDFs, and Context Binding

  June 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Threat Modeling for Engineers: Assumptions as Interfaces

  May 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Time Is a Lie: Clocks, Causality, and Ordering

  April 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Backpressure as a Correctness Property: Stability Under Load

  March 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Idempotency Everywhere: Designing Safe Retries in Distributed APIs

  February 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust

• Protocol State Machines: Invariants, Events, and Recovery

  January 1, 2016 · 4 min — #research-notes#protocol-design#correctness#formal-methods#Rust