¶ Core Infrastructure for City OS: TraceFix, TeLLMe, and Verified Coordination
¶ Group Members: Sankeerth BharadwajUG, Jay H DuvvuriUG, Shreyaa SanjayUG , Alejandro SaltoHS, Rakshan SenthilHS, Vihaan RajagopalHS, Annika JeenaHS, Abhishek ShuklaHS
¶ Mentors: Professor Jorge Ortiz, Shuren Xia, Taqiya Ehsan, Oscar Wu
¶ Week 1
¶ Details
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: TeLLMe, 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
¶ TeLLMe: Sankeerth Bharadwaj
¶ Trace-Fix: Jay Duvvuri
¶ Goals
- Receive and understand the project as a whole and TraceFix's role
- Understand Verified coordination (using PlusCal, TLA+, TLC)
- Learn about PlusCal, TLA+, and TLC (Integration)
- Learn about TraceFix and its pipeline
¶ Quick Summary
- PlusCal = mathematical algorithmic language that translates a workflow into a language
- TLA+ = middle step that TLC can run on
- Process: convert PlusCal to TLA+ → TLC runs multiple scenarios on the TLA+ code → find instances of deadlock, miscommunication with protocol, etc.
Trace-Fix works closely with Verified-Coordination's TLC Checker to conduct a protocol repair loop. A 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.
¶ Full Breakdown:
Given a task or description, a Protocol Topology is formed, and this is done by the LLM. The LLM creates a 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. (REPETITIVE PROCESS)
Week 1 had us read through the Trace-Fix paper[1], understanding the concepts and learning the pipeline structure and flow.
¶ Verified-Coordination: Shreyaa Sanjay
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
¶ Details
Weeks 2-4 had us work on the actual code and understand it. Our mission for Week 2 was to understand how the code worked, what the files did, and how each part fit together. When going into Week 3, our mind was fixated on making a seamless client-side application, a program which will create a UI for us to use to play with the code and the procedure.
¶ TeLLMe
Tellme pipeline:
¶ TraceFix
¶ Goals
- Make basic system design pipeline with a single agent orchestrator and multiple pipelines (for a single agent and multiple agents)
- Give LLM’s as little room for error as possible by tightening the context window (info available to LLMs) → Include checkpoints at each step of the design
¶ Simple System Design Pipeline
¶ Week 3
¶ Details
¶ TeLLMe
¶ Goals
- Began to implement an idea of an agent orchestrator which has a few responsibilities:
- Receives broken down natural language query from TeLLMe
- Decides whether the TraceFix pipeline is to be handled by a single agent or by multiple agents.
- Designed a prototype pipeline for TeLLMe + TraceFix
¶ TraceFix
¶ Goals
- Run TraceFix and figure out its limitations (TraceFix Prompting)
- Finish demo for single agent (without TraceFix) before Tuesday
- Outlined UI for TraceFix pipeline (Custom & Benchmark Tasks for finding errors)
¶ Viewer Visualization
¶ Viewer Runner
¶ Week 4
¶ Details
¶ TeLLMe
¶ New Simplified Pipeline
- Scrapped the agent orchestrator complex pipeline and replaced it with a more simpler and understandable pipeline:
- All components and technology incorporated to perform a task and ensure a correct answer.
¶ Goals
- Reworked the Intent Decomposition section of TeLLMe and implemented a basic Streamlit UI
- Now provides the user with a full range of information about what information TeLLMe received from their question
- Simply made the agent orchestrator a part of our TaskSpec pipeline instead of building the whole channel around it.
- Also provides the user with a complete pipeline example and status on the response.
¶ TraceFix
¶ Goals
- Found out that gpt 4.1 and 5 nano were not strong enough to run the pipeline; Waiting on a new API Key
- Established new Trace-Fix UI with workspace and runtime monitor implemented
¶ Updated TraceFix UI
¶ Updates
- UI changed to include a workspace
- Workspace: all the information that the agents need to execute the code
- Working on CityOS integration
- CityOS: privacy layer that adds noise to data and protects the identity of the people involved
- Running processes in CityOS requires running them as applications with a Dockerfile
¶ ## References
[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.