Formal-Verification

• The Curry-Howard Correspondence: How Type Theory Bridges Proof and Computation · 2025-03-18

  Explore the profound isomorphism between logical proofs and computer programs: how the Curry-Howard correspondence unifies propositional logic with typed lambda calculus, and how it enables modern proof assistants like Coq, Lean, and Agda.

• CHERI and Capability Hardware: Memory Safety at the Gate Level · 2025-03-11

  How CHERI Concentrate compression, the load barrier for temporal safety, and the Arm Morello prototype are reshaping what it means to build a secure processor — and why formal verification of capability integrity is the hard part.

• Smart Contract Security: Reentrancy, Front-Running, and Verification with Certora and Foundry · 2023-09-15

  A rigorous treatment of smart contract vulnerabilities—reentrancy, integer overflow, front-running/sandwich attacks—and the modern verification toolkit including the Certora Prover and Foundry fuzzing framework.

• Formal Verification of Cryptographic Protocols: ProVerif, Tamarin, and the TLS 1.3 Verification Story · 2023-04-06

  An exploration of the Dolev-Yao model, ProVerif and Tamarin provers, computational soundness results, and how formal methods proved TLS 1.3 secure before deployment.

• Abstract Interpretation: The Cousot Framework, Galois Connections, and Sound Static Analysis by Construction · 2022-01-20

  A rigorous exploration of abstract interpretation—Patrick and Radhia Cousot's unifying framework for static program analysis, from Galois connections to widening operators and the soundness proofs that guarantee analysis correctness.