Week 1 of this project had us go through the pipeline which has already been developed before and had us get familiar with it. What we were left with were 3 distinct pieces: ConcordFS, Tracefix and Verified Coordination. The work we did for each section and the deliverables we did will be listed below:
We spent this week reading previous literature and gaining more practice with the tools we will use before we get the code
Trace-Fix works closely with Verified-Coordination's TLC Checker to conduct a protocol repair loop. More on this will be said later on in this page. Basic overview of this portion is translating traces given out from the TLC Checker into LLM readable language. A specialized LLM repair agent will receive that language and do the repairs needed accordingly.
Given a task or description, a Protocol Topology is formed, and this is by the LLM. The LLM creates PlusCal code protocol, and this is sent to the TLC Checker. What the checker does is go through all possible corner scenarios and send back telemetry objects called traces. These traces are strings which the Trace-Fix translates to LLM language letting it fix the PlusCal code. THIS IS A REPETITIVE PROCESS.
Example of translated trace code for LLM Repair Agent:
Week 1 had us read through the Trace-Fix paper[1] understanding the concepts and learning the pipeline structure and flow.
During week 1, I practiced writing a PlusCal script given a protocol topology and running the TLC model checker using the PlusCal code. I successfully ran TLC on a script that generated no errors and wrote a PlusCal script with channel safety invariants broken to generate a TLC response that caught the error. In the future, I hope to use the LLM's already in place in the TraceFix pipeline to figure out how to implement the checker in the smart city agentic stack.
Week 2-4 had us work on the actual code, understand it. Our mission for Week 2 was to understand how the code worked what the files do and all. When going into Week 3 our mind was fixated on making a seamless client side application, a program whcih will create a UI for us to use to play with the code and the procedure.
[1] S. Xia, Q. Li, T. Ehsan, and J. Ortiz, "TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples," in *Proceedings of the 2026 ACM Conference on AI in System Software (ACM CAIS)*, 2026.