Yes, but engineers also need to search for a specification.
If an engineer tries to write a formal specification, they’re preparing themselves for a cold, humiliating shower.
After attempting this several times, I wish I’d started with formal methods much earlier.
So at the start, specification research is the big issue.
One area where AI can help enormously is the structural specification: collecting all notifications and request/reply events, data structures (even at a high level), all actors, all invariants, etc. This is massive work, very time-consuming, and AI can collect it fast.
Then it gets harder.
For every behaviour, a state machine must be defined — i.e., for each actor, for each possible notification or request that actor can receive, in each possible state that actor can be in.
This means that until the knowledge-accumulation problem is solved for both the structural and behavioral specifications, there’s no trust moat yet.
Once all the specification knowledge is collected and formalized, it has to be rewritten — no specification survives contact with the real world.
That’s the moment where the moat you mentioned is actually encountered: not only did the initial draft specification probably miss something, but we also need to trust what was written as the initial implementation of it.
Deterministic simulation testing, together with hierarchical state machines, is what lets the programmer explore the specification against reality and cross that moat.
But there’s an ocean before a spec is even good enough for the real world.
That’s where a concept database with the right meta-model can support the programmer.
ConceptBase, with its O-Telos data model, unlimited instantiation levels, and deductive rules, is a good candidate substrate — not because deduction validates the spec (that’s DST’s job), but because it lets most of the collected knowledge be derived rather than written by hand: actors, events, and invariants entered once at one abstraction level can be propagated, classified, and cross-referenced automatically across the others.
Hooked up via MCP, an AI agent can populate and query this continuously, doing by machine what would take a person months by hand.
The remaining hard problem is the mapping: designing the meta-model so that collection is mostly derivation, while DST remains the tool that actually explores whether the spec holds up.