You’ve been there: When you ask an LLM to construct a function, it returns something that is nearly functional but ignores restrictions, fails on edge cases, or generates untestable spaghetti.
What if I told you that LLMs could be trained to act like disciplined engineers?
The secret tactic that most developers don’t employ is that:
LLMs behave more consistently and produce better software when you organise your prompts using formal methods concepts.
Although formal methods are frequently taught in Computer Science degrees, engineers sometimes forget them once they graduate.
In practice, these ideas can result in less buggy, deterministic, testable, safe, and maintainable code when applied to LLM prompts.
I’ll go over how to use formal methods concepts to guide LLMs across the software engineering lifecycle.
TL;DR: Use preconditions, postconditions, invariants, state machines, and formal properties to organise your LLM prompts. LLMs produce significantly better code in response to formal structure.
Invariants, Preconditions, and Postconditions
Using preconditions, postconditions, and invariants to express software behaviour
These ideas are well understood by LLMs, who can adhere to them almost like code contracts.
Function Implementation
Function: calculate_discount(cart)
Preconditions:
- cart.items.length > 0
- every item has price > 0
- cart.user has a valid membership
Postconditions:
- return a numeric discount between 0 and price_sum
- VIP users get at least 5% discount
- normal users get ≤ 5%
Invariants:
- discount never becomes negative
- discount <= total cart value
Write Python code implementing this behavior.
Using this structure improves correctness and clarity in generated code.
Using Formal Proof Style to Reason About Correctness
You have strong proof skills because of your background in discrete maths and theory of computing, even though you may not have studied formal program logic.
This enables you to organise prompts for methodical bug identification and analysis:
{P} Code {Q}
Meaning: If precondition P holds, executing the code guarantees Q.
When debugging, this is perfect.
Example: Bugfix
# Specification
Preconditions:
- user_id exists
- database connection is active
Postconditions:
- function returns user profile
- no unhandled exceptions
- database handle is released
# Code
[paste code]
# Task
Check whether the code satisfies the postconditions.
Identify violations and correct the implementation.
This forces the LLM to:
- Identify underlying problems
- Reason methodically
- Refrain from damaging the interface
State Machines for Distributed Systems, Frontend, and APIs
One of the most effective formal tools for prompting LLMs is the state machine.
Beneficial for:
- UI flows
- Verification
- Forms with multiple steps
- Background employment
- Flows of payment
- WebSockets
- Tasks for IoT devices
Example Prompt (React UI Flow)
System: Checkout UI
States:
- idle
- entering_address
- reviewing_order
- processing_payment
- success
- error
Transitions:
idle → entering_address [on "Checkout"]
entering_address → reviewing_order [on valid form]
reviewing_order → processing_payment [on "Pay"]
processing_payment → success [payment_ok]
processing_payment → error [payment_failed]
Task:
Generate a React component that implements this state machine.
Use clean reducer logic.
This yields highly structured, bug-free UI code.
Relational Style System Modelling
Database constraints and business logic can be modelled using relational and set-based reasoning.
Beneficial for:
- Access control logic
- Database schema design
- Social media
- Systems for inventory
- Modelling business rules
Example Prompt (Inventory Logic)
SET User
SET Product
REL purchase: User → Product
Constraints:
- stock >= 0
- every purchase reduces stock by 1
- users cannot buy items with zero stock
- stock changes are atomic
Generate:
1. Django models
2. Business logic for purchase()
3. Enforcement of constraints
4. Unit tests validating invariants
The LLM can generate code that respects these constraints.
Creating Safe Code with Invariants
Consistency is ensured by invariants in systems such as:
- Transactions involving money
- Management of stocks
- Management of sessions
- Caching layers
Example Prompt (Money Transfer)
System Invariants:
- balance(user) >= 0 always
- total money in system is conserved
- transfer is atomic
- no two transfers can operate on same account concurrently
Task:
Write a safe money_transfer() function in Go using mutexes.
Include unit tests proving invariants.
You can expect solid and safe code output.
Algebraic Specifications for API Contracts
Focusing on operations and equations helps define clear API behavior.
Example Prompt (Rest API Spec)
Operation: add_to_cart(user, product)
Axioms:
1. add_to_cart(cart, p) then get_cart(cart) includes p
2. remove_from_cart(cart, p) then get_cart(cart) excludes p
3. idempotency: add_to_cart(cart, p) twice is same as once
4. removing non-existing items has no effect
Generate:
- FastAPI routes
- Pydantic models
- Business logic
- Tests verifying axioms
This produces robust and predictable API implementations.
Incremental Refinement to Build Complex Features
Start with an abstract specification and refine step-by-step.
Example Multi-Step Prompt
Step 1:
Write an abstract specification for a real-time fuel economy meter.
Step 2:
Refine it into a hardware design (Arduino + sensors).
Step 3:
Refine it into a Python API for receiving sensor data.
Step 4:
Refine it into a React dashboard UI.
Each step refines and implements the previous abstraction.
Formal Testing Prompts (Property-Based Testing)
Formal methods emphasize properties, not just examples. LLMs can generate property-based tests easily.
Example Prompt
Write property-based tests for the function sort(numbers).
Properties:
- output is sorted ascending
- output contains same multiset as input
- length is unchanged
- idempotent: sort(sort(a)) == sort(a)
Each stage becomes a provable refinement of the previous stage.
Now let’s look at how formal methods can improve your tests.
Verification Style Prompts (Proof Obligations)
You can ask LLMs to verify correctness by stating formal obligations.
Example Prompt
Check whether this implementation satisfies:
O1: No null user can place an order
O2: Stock never becomes negative
O3: Order total is consistent with item prices
O4: Operation is atomic
If any obligation fails, fix the implementation.
This produces extremely safe code.
Formal Methods in Architecture & System Design
You can express system-level properties with:
- State machines
- Invariants
- Consistency guarantees
Example Prompt
System: E-commerce microservice architecture
Guarantees:
- eventual consistency across cart, order, inventory
- exactly-once order creation
- idempotent payment processing
- saga rollback on failure
Generate:
- high-level architecture
- service boundaries
- async workflows
- compensation actions
This yields professional system designs.
Final Thoughts
LLMs are powerful, but to harness them fully, treat them like disciplined engineers:
- Give clear specifications
- Define constraints
- Set invariants
- Describe states
- Impose correctness rules
This structured, formal-methods–style prompting consistently produces:
- Better code
- Fewer bugs
- Clear architecture
- Safer systems
- More predictable outputs
If you want reliability from LLMs, leveraging these formal concepts is your strongest tool.
Inspired from Dominik Tornow’s post.
Formal Methods Recommended Reading List
-
Discrete Mathematics and Logic Foundations “Discrete Mathematics and Its Applications” by Kenneth H. Rosen
-
Theory of Computation and Automata “Introduction to the Theory of Computation” by Michael Sipser
-
Software Engineering & Specification Modeling “Software Engineering: A Practitioner’s Approach” by Roger S. Pressman
-
Formal Specification and Relational Models “Software Abstractions: Logic, Language, and Analysis” by Daniel Jackson
-
Concurrency and Invariants “Operating System Concepts” by Abraham Silberschatz, Peter Baer Galvin, Greg Gagne
-
Property-Based Testing and Verification “The Art of Software Testing” by Glenford J. Myers, Corey Sandler, Tom Badgett