Abstract PeerCheck [1] is a lightweight library-based approach to implement symbolic execution over object-oriented languages without modifying the analyzed code. Unlike traditional symbolic execution engines, the symbolic semantics is built as an external library that runs together with the target program. They can accomplish this task thanks to special features of the python programming language which allows one to implement symbolic values with class objects. However, their approach is limited to symbolic execution on primitive types. In this work, we show an extension that enables one to perform symbolic execution with user-defined class objects. In addition, we build a new verification tool, called PEF, which implements the described technique, and our extension. This tool can be used to verify programs written in the Python programming language, and we developed in python on top of the Z3 SMT solver. We used the tool to verify its own code, showing its potential and usefulness to test programs in production. We also evaluate the tool for testing well known algorithms and data structures.