Posts tagged #security
-
Verified Security Gates: Safe ML Deserialization
Using Lean 4 soundness proofs to gate Python type-stub deserialization in the Falcon-secure project.
-
Counterfactual Provenance Experiments: Stress-Testing Token Roles
Analyzing the Counterfactual V2 results—how the model behaves when provenance signals are zeroed or adversarial.
-
Lean 4 as a Soundness Oracle for Security Properties
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.
-
Pickle Is a CVE Factory; Type Stubs Are the Gate
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.
-
The Pre-W Learnable Role-Angle Mechanism: RoPE-Provenance
Moving beyond fixed π/2 offsets to learnable provenance rotations and the 'pre-W' transport interpretation.
-
From Bug Fix to Production Hardening: A Refactoring Marathon
Stalled task detection, security hardening, code refactoring, and lifecycle signals — turning a task queue into production-grade infrastructure.