Automate and accelerate
production using
math proofs.
Symbolia verifies the software that runs your machines.
Explore the demoChange the software.
See what happens.
This robot welds a square.
Interactive controller demo
Ready to begin.
State 1 of 6 Command permission: disabledAll protections on.
All checks pass
All controller checks pass.
Proof tree
Controller behaviourEstablished
Four controller checks
How the controller handles stop, start, reset and completion signals.
A curtain trip disables commandsEstablished
When the curtain trips, the controller stops allowing movement at its next update.
Starting needs a new start signalEstablished
The weld begins only when the start signal changes from off to on.
Reset does not restart the weldEstablished
Reset returns the controller to ready. Starting the weld is a separate action.
Only the current edge can advance the jobEstablished
A completion signal for a different edge cannot move the sequence forward.
A complete runEstablished
One possible-run check
The sequence draws all four sides and closes the square.
The sequence completes all four edgesEstablished
The example sequence completes all four edges.
Where this result appliesEstablished
This result applies to the selected controller and settings.
What still needs checking on the machineOpen
Three assumptions and two open checks
Equipment response, sensors, weld quality and deployment readiness.
The equipment follows the controllerAssumed
The robot and laser respond to the controller’s commands.
Curtain trips are detected in timeAssumed
Curtain trips reach the controller in time to stop the machine.
Completion signals are trustworthyAssumed
Each completion signal corresponds to a finished edge.
The weld meets the required qualityOpen
Check weld strength, consistency and finish.
The machine is ready to deployOpen
Complete the machine’s safety and integration review.