Currently Isabelle is the only proof assistant capable of speaking PGIP. Once the definition of PGIP matures and sees a formal release, it will be interesting to see how easily other proof assistants can incorporate this system.
