My inspiration for this project came from the challenges faced by companies like Bank of America, burdened by legacy code written in various languages. Migrating to a more secure and performant language is often hindered by the complex and error-prone process of code re-implementation.
I decided to tackle this problem by creating CIVL-X, a proof assistant that allows writing verification on top of existing code, regardless of the language.
My journey began by diving into the admittedly challenging world of Smalltalk. Parsing its unique syntax and semantics proved to be a time-consuming but rewarding endeavor. The learning curve was steep, but I'm proud of the parser I built.
Another hurdle emerged when integrating the powerful Z3 SMT solver. C to Rust bindings caused unexpected roadblocks, extending the development timeline. Additionally, I ambitiously attempted to incorporate a GitHub bot, but it remains a work in progress.
Despite these challenges, I'm satisfied with the initial functionality of CIVL-X. Currently, it can handle comparisons and assignments, laying the groundwork for future development. Overall, this project was a valuable learning experience, pushing me to expand my technical skills and gain a deeper understanding of code verification and legacy code management.
Log in or sign up for Devpost to join the conversation.