LFX Mentorship Active 2026
Formal Methods for Refactoring
About the Organization
<p><strong>*APPLICATION ONLY OPEN TO COLLEGE STUDENTS BASED IN CHINA*</strong></p><p><br></p><p><strong>Problem Statement</strong></p><p><br></p><p>Software refactoring and restructuring is common in the open-source development of SONiC. Existing code structure may limit the adoption of new usage scenarios or protocol features, necessitating its refactoring into a better logical structure. For example, the ongoing RIB/FIB project intends to separate the RIB and FIB maintenance code in Zebra and move the latter down to SONiC’s fpmsyncd component. Since fpmsyncd resides in SONiC code space, it allows FIB to construct SONiC specific forwarding chain, and handle route convergence based on SONiC’s requirements.</p><p><br></p><p><br></p><p><strong>Mentorship Objectives</strong></p><p><br></p><p>A central requirement in such refactoring is to ensure that behavior changes are exactly as expected. In the RIB/FIB example, it requires that normal executions must be equivalent before and after the refactor. The objective of this mentorship is to devise a systematic approach to validate behavioral equivalence during SONiC refactoring. More specifically, it involves applying formal methods to mathematically describe the intended behavior, compare two distinct setups, and generate comprehensive tests to ensure the consistency before and after the refactor. This will serve as an exemplar of the formal-methods-based correctness paradigm in production code development.</p><p><br></p><p><br></p><p><strong>Expected Outcomes and Deliverables</strong></p><p><br></p><ul><li>Abstract formal models describing expected behavior of the relevant RIB/FIB operations.</li><li>Testing infrastructure that supports parametrized testing of individual modules and execution sequences across modules.</li><li>A test generation framework and the resulting high-coverage benchmark to validate the correctness of the RIB/FIB implementation.</li><li>*<strong>Program Term: Summer / Fall Term (May - November) 20 hours of work each week*</strong></li></ul><p><br></p><p><br></p><p><strong>Recommended Qualifications</strong></p><p><br></p><ul><li>Familiarity with Python and C/C++</li><li>Basic understanding of network forwarding and routing</li><li>Comfort with hands-on systems work under technical guidance, including system setups, trouble shooting, etc.</li><li>Strong communication skills</li></ul>
Primary Technologies & Languages
pythoncc++
Technical Topics & Focus Areas
pythoncc++
Participation Years
Completed Projects Distribution
Annual Completed Projects History
Formal Methods for RefactoringHover over bars to view completed counts
4
3
2
1
0
2026
Projects1
Years Active1
Stackpython
TierTier 1
Past Projects
Showing 1 of 1 projects. Click any project card for scope, mentors, and proposal studio.
Ensuring Behavioral Equivalence in SONiC’s RIB/FIB Architecture
Intermediate<p><strong>*APPLICATION ONLY OPEN TO COLLEGE STUDENTS BASED IN CHINA*</strong></p><p><br></p><p><strong>Problem Statement</strong></p><p><br></p><p>Software refactoring and restructuring is common in the open-source development of SONiC. Existing code structure may limit the adoption of new usage scenarios or protocol features, necessitating its refactoring into a better logical structure. For example, the ongoing RIB/FIB project intends to separate the RIB and FIB maintenance code in Zebra and move the latter down to SONiC’s fpmsyncd component. Since fpmsyncd resides in SONiC code space, it allows FIB to construct SONiC specific forwarding chain, and handle route convergence based on SONiC’s requirements.</p><p><br></p><p><br></p><p><strong>Mentorship Objectives</strong></p><p><br></p><p>A central requirement in such refactoring is to ensure that behavior changes are exactly as expected. In the RIB/FIB example, it requires that normal executions must be equivalent before and after the refactor. The objective of this mentorship is to devise a systematic approach to validate behavioral equivalence during SONiC refactoring. More specifically, it involves applying formal methods to mathematically describe the intended behavior, compare two distinct setups, and generate comprehensive tests to ensure the consistency before and after the refactor. This will serve as an exemplar of the formal-methods-based correctness paradigm in production code development.</p><p><br></p><p><br></p><p><strong>Expected Outcomes and Deliverables</strong></p><p><br></p><ul><li>Abstract formal models describing expected behavior of the relevant RIB/FIB operations.</li><li>Testing infrastructure that supports parametrized testing of individual modules and execution sequences across modules.</li><li>A test generation framework and the resulting high-coverage benchmark to validate the correctness of the RIB/FIB implementation.</li><li>*<strong>Program Term: Summer / Fall Term (May - November) 20 hours of work each week*</strong></li></ul><p><br></p><p><br></p><p><strong>Recommended Qualifications</strong></p><p><br></p><ul><li>Familiarity with Python and C/C++</li><li>Basic understanding of network forwarding and routing</li><li>Comfort with hands-on systems work under technical guidance, including system setups, trouble shooting, etc.</li><li>Strong communication skills</li></ul>