Formal Methods

TL;DR for operators ProbGuard1 is a runtime safety monitor that tries to answer a more useful question than “Has the agent broken a rule?” It asks: “Given where the agent is now, how likely is it to end up breaking a rule soon?” That shift matters. Many agent failures are not single bad actions. They are bad trajectories: the robot chooses the wrong object, the car carries too much speed into a risky scene, the workflow skips a confirmation step three moves before data is exposed. A conventional rule-based guardrail often detects the problem when the violation is already visible. ProbGuard tries to detect the probability mass moving toward the violation earlier. ...

TL;DR for operators Hospital bed allocation is not just “find an empty bed.” It is a rolling constraint problem: patients arrive, diagnoses imply treatment trajectories, treatment phases require different levels of care, rooms have different capacities and monitoring categories, some patients cannot share rooms, hospital policy may forbid mixed-gender rooms, and moving patients unnecessarily is bad practice. Yes, the spreadsheet is sweating. ...