I just started using Frama-C [1] for analyzing some of our embedded C programs. Pretty awesome suite of tools. Especially its ability to describe and verify function contracts with ACSL [2]. The tool suite is primarily build with OCaml. Has anyone considered building a Haskell interface to Frama-C? I lack the expertise and time for such a project. But it sure would be nice to be able to write verification plug-ins with Haskell. -Tom [1] http://frama-c.com/ [2] http://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language