Type-Stub Security Gates for ML Deserialization

Pickle is a CVE factory. falcon-secure uses Python type stubs and Lean 4 soundness proofs to gate unsafe deserialization at the type-checker level.

1. Pickle Is a CVE Factory; Type Stubs Are the Gate

   May 1, 2026

   Every ML project eventually loads a pickle file. This is a problem: pickle can execute arbitrary Python on deserialization. Here is how falcon-secure uses Python type stubs to make unsafe loads a static type error.

   #security #python #pickle #ml-ops #type-stubs

2. Lean 4 as a Soundness Oracle for Security Properties

   May 2, 2026

   Type stubs catch misuse at type-check time. But can we prove they are sound — that a well-typed program cannot trigger the dangerous code path? Enter Lean 4.

   #security #lean4 #formal-verification #python #type-theory