WINLAB Summer Internship

From a Prompt to Verified Agent Applications

August 2026

Jorge Ortiz

NSF CS3 WINLAB COSMOS TraceFix project TeLLMe paper CityOS paper

This summer I worked with 16 WINLAB interns on an agentic stack that translates a natural-language prompt into a working distributed application. Before planning begins, TeLLMe determines which operations the application may perform and which data it may use. The planner receives only that constrained set. TraceFix generates the coordination protocol and uses TLC to check its distributed execution properties. The CityOS Synthesizer then packages the agents and their monitor as containerized CityOS applications. CityOS is a privacy-oriented edge runtime that executes applications in isolated containers. Its APIs control how each application can access sensor data. The Smart Room and CARLA supplied two environments in which the students could run and evaluate the resulting applications. The NSF-funded Center for Smart Streetscapes, or CS3, supported the four projects that made this work possible.

×

A prompt becomes a distributed application

The stack sends each prompt through a compiler that constrains what the resulting agents can execute. TeLLMe analyzes the request before it calls a language model. It then identifies the available capabilities and determines which operations and data the application may use. Those capabilities come from the environment in which the application will run. In the Smart Room, they come from the cameras installed in the room and the CityOS services that expose their recordings. In CARLA, they come from simulated sensors and the state interfaces provided by the simulator. TeLLMe therefore builds the plan from the sensing modalities available in each environment. The planner sees only that constrained set, and a deterministic validator checks its output. TraceFix converts the validated plan into a PlusCal coordination protocol. The Synthesizer uses the verified protocol to generate an application for each agent and a monitor for the coordination state.

Students and mentors

Eight undergraduate students worked alongside eight high school students from May 26 through August 7. We organized them into four CS3-funded project groups. The core infrastructure group implemented the prompt-to-application path. The Smart Room and CARLA groups supplied physical and simulated environments in which the generated applications could operate. The GroundingEval group checked their results against recorded scene state. Because the generated agents exchanged data through declared channels, the evaluation system could inspect the artifacts returned with each answer.

The Smart Room became a CityOS node

Crystal Burbano, Alan Jiang, and Eliana Nuñez

Crystal, Alan, and Eliana turned the Smart Room into a CityOS sensing node. We needed each recording to carry enough context for another service to inspect what happened. Their run folders therefore include the video, an event record, metadata, validation results, and logs. CityOS can route the resulting evidence because the room processes and packages it locally.

The first implementation assumed that a Raspberry Pi 4 could capture and encode several camera streams concurrently. The processor could not sustain both operations, so the students separated capture from encoding and processed each recording after the run. The radar produced a different problem. Its measurements were internally consistent, but the reported distances of 200 or 500 centimeters corresponded to a wall. The system was measuring the wrong part of the room. The students therefore removed radar from the demonstration and used the cameras to produce evidence about presence and activity.

Tests on the Smart Room recordings also changed the vision pipeline. RTM pose reduced skeleton jitter, while RGB-based SlowFast-AVA recognized activities directly from the frames. RealSense hardware timestamps assigned a capture time to each frame, and controlled light flickers provided a common reference for synchronizing cameras. The group then wrote spatial and temporal questions whose answers could be checked against the recordings.

Smart Room project page

The agentic stack produced verified applications

Sankeerth Bharadwaj, Jay H Duvvuri, Shreyaa Sanjay, Alejandro Salto, Rakshan Senthi, Vihaan Rajagopal, Annika Jeena, and Abhishek Shukla

Sankeerth, Jay, Shreyaa, Alejandro, Rakshan, Vihaan, Annika, and Abhishek connected TeLLMe and TraceFix to a new CityOS Synthesizer. TeLLMe turns a natural-language request into a validated task specification. The planner receives only the operations and data that TeLLMe has permitted. TraceFix converts that specification into a PlusCal coordination protocol and asks the TLC model checker to explore its possible executions. When TLC finds a deadlock or a channel-safety violation, the repair agent uses the counterexample trace to revise the protocol. The Synthesizer packages the verified agents and their monitor as containerized CityOS applications.

We placed the verification logic in TraceFix and kept it outside the deployment path. TraceFix establishes the protocol properties of the distributed application. The Synthesizer preserves the verified plan while translating it into deployable CityOS applications, and CityOS runs those applications within their declared privacy boundaries. This separation allows the packaging and runtime to change without changing the coordination properties checked by TLC.

The most visible performance problem was that a run could take about 20 minutes. The original path invoked a model-driven repair loop even when the incoming request matched a coordination pattern we had already verified. The students built a deterministic classifier that recognizes those patterns and reuses the corresponding template when the match is strong enough. Runtime fell to between 20 and 30 seconds, a 98.3 percent reduction, while TLC continued to check every selected protocol before synthesis.

Run summary

Route

Single agent

How TraceFix will coordinate the application.

Task category

Occupancy count

The kind of question represented by the request.

Harnesses

2

Two evidence-gathering units were selected.

Validation

Accepted

The proposal passed its deterministic check.

Privacy

Bounded

The application operates within the CityOS structured-context scope.

Evidence card

Descriptive

The front-facing card the answer must fill.

Two interfaces remain incomplete. One orchestration interface has not been connected, and the answer agent can still call the Smart Room API instead of relying on the data admitted through its application boundary. The CityOS application model supplies the mechanism for privacy enforcement, but this direct path has to be removed before we can make an end-to-end privacy claim for the demonstration. A subsequent implementation will close both paths and require the answer agent to operate only on the inputs declared in its plan.

Core infrastructure project page

CARLA supplied a controlled synthetic sensor

Ryan Purakal and Ryan Baik

Ryan Purakal and Ryan Baik gave us a second way to observe an environment. Their CARLA application turns a natural-language request into a structured scenario, runs the scenario, and writes evidence in the same format as the Smart Room. We can repeat a traffic condition with known parameters because the simulator becomes a synthetic CityOS sensor.

The students moved the view from a vehicle dashboard to fixed infrastructure at a Town10HD intersection. Overhead cameras observed the scene alongside LiDAR, radar, segmentation output, and vehicle telemetry. Six runs with the same seed produced the same event structure, although the vehicle dynamics drifted by as much as 2.67 meters per second. Another experiment held the seed and traffic fixed while changing the weather, which let the team isolate the effect of weather on the observations.

The structured checker validated the recorded fields but did not establish that a vehicle's orientation agreed with its motion. Video review exposed a case in which the vehicle moved without turning its yaw toward the direction of travel. This result gives us an additional visual consistency check for future runs. Ryan Baik also imported OpenStreetMap data for New Brunswick through Blender and Unreal Engine, providing a path from preset CARLA towns to experiments based on streets around Rutgers.

CARLA project page

GroundingEval defined what the scene contained

Maj Globocnik, Vikhyat Kulshrestha, and Aryan Mittal

Maj, Vikhyat, and Aryan worked on the question that sits underneath the entire demonstration. What should count as the correct answer for a scene? Their GroundingEval pipeline builds the ground-truth record from the internal state of CARLA. Each frame records the objects and their state, location, visibility, and relations to named zones. A person can exist in the simulator while remaining outside the view of a camera, so the record has to state visibility explicitly.

The students separated what a scenario intended to produce from what CARLA measured during execution. A third document records the comparison. Fields such as the map and actor count must match exactly, while the report records timing and spawn-position differences with tolerances. This separation lets us see whether a scenario ran as requested before we use it to judge the answer from TeLLMe.

The evaluation pipeline required its own validation before it could be used to judge the other components. The students derived location difficulty from the structure of the road network and independently checked 146 zone polygons. That check exposed two converter errors in a new CARLA format. Independent validation found no mismatches in the first batch of 30 low-tier scenarios, after which the CARLA group could begin bulk execution.

GroundingEval project page

Integration

The principal integration result was a path from a prompt to a set of deployable agents with explicit policy and coordination constraints. TeLLMe limited the capabilities available to the planner. TraceFix checked the distributed protocol, and the Synthesizer preserved that protocol in the generated CityOS applications and monitor. The final presentation exercised those applications over two environments with different sources of uncertainty. The Smart Room produced observations from physical sensors, while CARLA produced repeatable traces and exposed simulator state as ground truth.

The evidence path tested whether the generated applications operated on valid observations. The radar data satisfied its expected format and described the distance to a wall. That reading missed the event under observation. The students removed the radar because preserving the interface would have preserved the wrong interpretation of the scene. In CARLA, the structured checker accepted a trajectory whose yaw was inconsistent with the direction of travel. The video exposed this condition because schema validation alone could not establish that the recorded state represented plausible motion.

Execution time exposed a separate limitation. TraceFix invoked the model-driven repair loop even when a request matched a coordination pattern that had already been verified, which increased runtime to about 20 minutes. Reusing a verified template reduced that path to between 20 and 30 seconds while retaining TLC as a check before synthesis. The next iteration will keep the common evidence and coordination interfaces while adding Smart Room recordings and New Brunswick CARLA scenarios. It will also restrict the answer agents to supplied evidence and extend GroundingEval to distinguish simulator state from what a camera could observe.