PVSGym

A Reinforcement Learning Environment for PVS

PVSGym is a reinforcement learning environment built around the PVS theorem prover. It enables research on automated proof synthesis with access to expert-level NASALib proof rollouts and a JSON-RPC interface for agents.

Features

JSON-RPC proof interaction API
NASALib dataset: 21k+ proof rollouts
Integrates symbolic reasoning and reinforcement learning

Click here to explore NASALib Library

Read our openreview paper.

Play with the demo in Huggingface spaces

You can pip install PVSgym as `pip install git+https://github.com/manoja328/pvsgym.git` or browse the source PVSgym github

If you use PVSGym in your work, please cite it as follows:

@misc{pvsgym2025,
  title={PVSGym: A Proof Learning Environment},
  author={Acharya, Manoj and Nukala, Karthik and Shankar, Natarajan},
  year={2025},
  howpublished={https://github.com/sri-csl/pvsgym}
}

@misc{nasalib2024,
  title={NASALib: NASA PVS Library},
  author={NASA Formal Methods Team},
  year={2024},
  howpublished={https://github.com/nasa/pvslib}
}