-
Changing the frame: Formal modeling with LLM assistance, Part 1
Tools for formal modeling have so far favored generality and lack of constraints over well-adaptedness and safeguards. The emergence of LLMs is changing the balance by making it easier to create formal artifacts but harder to be confident in their reliability. Next-generation technology for formal modeling should meet this moment by situating models within more constrained frames, while enabling the frame to be fluidly shifted when circumstances demand.
-
alifib, the language of higher-dimensional diagrams
alifib is an experimental programming language and interactive proof assistant in which programs are diagrams — not illustrations of programs, but the syntax itself, the internal representation, and the thing that is checked and run.
-
SDCPNs: A Common Language for Complex Systems
Formal guarantees of AI safety begin as a modelling problem: to reason rigorously about whether an AI-controlled system is safe, you first need a mathematical representation of that system. This post builds a Stochastic Dynamic Coloured Petri Net up from an ordinary Petri net, one feature at a time, and then uses three cyber-physical examples — an industrial gas supply chain, a truck fleet, and a semiconductor fab — to show the range of systems the resulting formalism can represent.
-
Why Supply Chains Are an Ideal Testbed for Safeguarded AI
Supply chains pair interrelated decisions with high-consequence outcomes, which is what makes them an ideal proving ground for Safeguarded AI — a world model that predicts an action’s consequences, an explicit specification of acceptable outcomes, and a verifier that can establish the system satisfies it.