PVS theorem prover

[Google Scholar] [Wikipedia]

Is a kind of: interactive theorem prover
Papers:

Putting it all together - Formal verification of the VAMP [beyer:ijsttt:2006]
Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]

The opinions expressed are my own views and not my employer’s.