Kestrel Institute hosts at least a few researchers like Dr. Kimmell who are working on applied formal methods that might one day be useful for proving the soundness of things like FAI bootstraping code.
“Equational Reasoning about Programs with General Recursion and Call By Value Semantics” includes work on how to reclaim sound reasoning about potentially unsound programs, even when they use general recursion and aren’t specified with constructive type theories that can rely on the Curry-Howard correspondance to automatically generate proofs from programs.
See on www.kestrel.edu
