Developed POSIX socket and I/O multiplexing API models for the esbmc/esbmc repository, enabling formal verification of networked C applications. The work involved implementing operational models for socket, recv, send, select, and poll functions, along with new header files and a comprehensive library to support robust network software verification. Regression tests were added to demonstrate both failure and success cases for buffer overflow vulnerabilities, ensuring model correctness and reproducibility. Utilizing C programming, formal verification, and system programming skills, this contribution expanded ESBMC’s verification coverage and established a foundation for stabilizing network-related features, directly supporting earlier vulnerability detection in network code.