This talk will cover joint work with Andrew Gordon at Microsoft Research this summer. Proving safety properties of security protocols is difficult. It is usually done by creating a formal model of the protocol and then doing the proofs on that model. In order for these proofs to apply to the actual source code, one would have to prove correspondances between the model and the code itself which often is even more difficult than the original proofs. Moreover, many proctocols used today do not even have a formal definition and the source code is as close as we get. We have created a type and effect system for F# and created a type checker for it which allows us to prove security properties on actual running source code.