Using Lean for Safety and Reinforcement Learning for Control: A Minimal Virtual Power Plant Project¶

Most discussions about virtual power plants (VPPs) and AI jump too quickly to performance: better bidding, better dispatch, better arbitrage, better forecasts.

That is useful, but it skips the harder question.

If a learning-based controller is making operational decisions for an energy system, how do we know it stays inside physical and operational limits? How do we know the simulator, the logged trajectory, and the safety model still mean the same thing after the code evolves?

That question is what motivated this project.

I built a small but complete prototype that combines:

Lean 4 for formalized VPP constraints and trace verification
Python for environment simulation and RL training
a JSON trace as the contract between the two sides

The goal was not to build a production-grade VPP stack. The goal was narrower and more useful:

show that formal verification and reinforcement learning can coexist in one practical engineering loop.

The Core Idea¶

The architecture is intentionally split into two responsibilities.

Reinforcement learning is responsible for searching for better decisions over time. Lean is responsible for defining what is never allowed to go wrong.

That is the key design choice.

I am not using Lean to synthesize the control policy. I am using Lean to define and check the safety envelope around the policy.

In practice, that means:

Python trains a controller on a simplified VPP environment
Python exports an episode trace
Lean parses that trace and verifies every step against the formal model

This division of labor maps well to how real control systems are often structured:

a flexible optimization or decision layer on top
a rigid, auditable safety layer underneath

What the Minimal VPP Model Includes¶

To keep the system small enough to reason about, the current prototype models a single-site VPP with only the most essential components:

one battery
one solar generation profile
one site load profile
grid import/export
buy and sell electricity prices

The state is deliberately tiny:

State = { soc }

The action is also deliberately tiny:

Action = { batteryDelta }

Here, batteryDelta represents the battery energy change at the current step:

positive means charging
negative means discharging
zero means idle

The net grid exchange is defined as:

netGrid = load - solar + batteryDelta

That gives a compact but useful system model:

higher load increases net grid demand
higher solar reduces net demand and may create export
charging the battery consumes additional energy at the site
discharging the battery offsets grid demand

This is not a full VPP market engine, but it is enough to support a full training-to-verification loop.

What Lean Formalizes¶

The most important Lean modules are VppLeanRl/Domain.lean and VppLeanRl/Trace.lean.

They define the formal meaning of the environment rather than just its implementation.

The current model checks four categories of constraints.

1. Parameter validity¶

Examples:

battery capacity must be positive
charge, discharge, and grid limits must be non-negative
degradation penalty must be non-negative

2. State validity¶

The battery state of charge must remain within bounds:

0 <= soc <= batteryCapacity

3. Action validity¶

An action is not judged in isolation. It is judged in context.

Lean checks that:

the battery delta stays within the charge limit
the battery delta stays within the discharge limit
the next state of charge stays within battery bounds
the resulting grid exchange stays within the allowed grid limit

That matters because many systems only clamp the raw action value and never formally check the actual consequence of applying that action to the current state.

4. Trace consistency¶

This is one of the most useful parts of the project.

Lean does not merely ask whether each step looks valid. It also checks whether the exported trace is internally consistent:

does the recorded state match the previous step's actual nextState?
does the exported nextState equal the result of the formal transition function?

This catches a class of bugs that are common in simulation-heavy systems: semantic drift between the environment, the logs, and the intended model.

Why the Python Side Is Intentionally Simple¶

The Python environment is implemented in vpp_rl/env.py.

I deliberately did not start with Gymnasium, Stable-Baselines3, PPO, or SAC.

Instead, I built a dependency-light environment and used a small tabular Q-learning baseline in vpp_rl/agent.py.

That was a deliberate engineering decision.

Reason 1: close the loop before scaling the stack¶

The first success criterion for this project is not algorithmic sophistication. It is semantic alignment.

Before introducing heavier RL tooling, I wanted to confirm that:

the environment definition makes sense
the Python and Lean semantics match
the trace export and verification flow works end to end

Reason 2: the current state space is small¶

The observation uses only:

the time index
the battery state of charge

That makes the state space small enough for a tabular baseline to be useful.

Reason 3: debugging is easier¶

When a policy behaves badly, a Q-table is much easier to inspect than a neural network. At this stage, transparency is more useful than sophistication.

Reward Design¶

The current reward is based on a simple cost model:

cost = buyPrice * gridImport
     - sellPrice * gridExport
     + degradationPenalty * abs(batteryDelta)

Training uses reward = -cost.

This encourages the controller to learn a recognizable pattern:

charge when electricity is cheap
discharge when electricity is expensive
exploit solar surplus when available
avoid unnecessary cycling because of battery degradation cost

This reward is intentionally simple. Its value is not realism; its value is clarity.

How Python and Lean Are Integrated¶

The integration mechanism is straightforward:

Python trains; Lean verifies. JSON is the contract.

After training, Python exports an episode trace containing:

params
initialState
each step's state
the exogenous signal
the chosen action
the resulting nextState

The Python data model in vpp_rl/model.py explicitly serializes field names in the form Lean expects, such as:

buy_price -> buyPrice
battery_delta -> batteryDelta
initial_state -> initialState

Lean then deserializes the trace and validates it step by step.

The verification command is:

lake env lean --run VppLeanRl/Cli.lean -- artifacts/episode_trace.json

If everything is consistent, Lean reports success and prints the final state.

If anything is inconsistent, such as an out-of-bounds SoC, an invalid grid exchange, or a mismatched nextState, verification fails.

What the Current Prototype Produces¶

I ran the complete flow locally with:

./scripts/run_demo.sh 200

One sample run produced:

episodes=200
training_reward=-992.0
greedy_reward=-936.0
idle_reward=-1087.0
improvement=151.0
trace_path=artifacts/episode_trace.json
trace verified; final state = { soc := 0 }

This result does not prove anything about real-world VPP economics. That would be an overclaim.

What it does show is the part that matters at this stage:

the RL baseline learned a policy better than the idle strategy in this deterministic setup
the generated trace passed Lean verification
the full train-export-verify loop works

That is the actual milestone.

Why This Architecture Matters¶

The practical value of this project is not the specific Q-learning baseline. It is the separation between control and trust.

If you scale this idea up, it offers at least three concrete advantages.

1. A safety envelope around learning-based control¶

The RL algorithm can change later. It could become PPO, SAC, DQN, or something multi-agent.

As long as the controller emits trajectories, Lean can remain the independent verifier of state transitions and constraint satisfaction.

2. Protection against semantic drift¶

Complex simulation systems often decay through small mismatches:

a field name changes
a transition rule changes
the logging format changes
the documentation lags behind the implementation

Trace verification provides a concrete mechanism for catching these mismatches early.

3. A path toward stronger formal guarantees¶

Right now, Lean verifies single-step safety and trace consistency. That is only the start.

The same architecture could be extended to reason about:

multi-step invariants
richer reward properties
more DER types
flexible loads
market bidding actions
stronger runtime safety filtering

What I Intentionally Did Not Build¶

Scope discipline matters here.

This project does not yet include:

deep RL policies
stochastic weather or load uncertainty
multiple batteries or multiple sites
market-clearing logic
a production scheduler or web service
visualization dashboards

That is intentional.

Trying to build a realistic simulator, a sophisticated RL stack, and a formal verification layer all at once is how projects become impressive demos with weak foundations.

This prototype does the smaller but harder thing first: it makes Lean and RL agree on the same system semantics.

What I Would Build Next¶

If I were continuing this project, I would prioritize three directions.

1. Upgrade the RL baseline¶

The natural next step is to replace tabular Q-learning with PPO, DQN, or SAC depending on whether the action space stays discrete or becomes continuous.

2. Enrich the VPP model¶

That means adding more realistic structure:

multiple DERs
demand response
forecast errors
network-side constraints
possibly market participation actions

3. Move from offline verification to online safety filtering¶

The current flow is:

Python generates a trajectory
Lean verifies it afterward

A stronger architecture would be:

the policy proposes an action
a formal safety layer rejects invalid actions in real time
only the filtered action reaches the environment

That is where formal methods stop being an audit layer and become part of the control loop itself.

Final Thought¶

This project is small, but it points at something important.

For critical infrastructure, it is not enough for AI controllers to be effective. They need to be auditable, bounded, and semantically trustworthy.

That is why I find the combination of Lean and reinforcement learning interesting.

RL helps search for useful decisions in sequential settings
Lean helps define what must remain true no matter what the policy wants to do

Those two capabilities are not in conflict. In systems like virtual power plants, they should probably be designed together.

How to Run the Project¶

lake build
python3 -m unittest discover -s tests
python3 -m vpp_rl.train --episodes 600 --output artifacts/episode_trace.json
lake env lean --run VppLeanRl/Cli.lean -- artifacts/episode_trace.json

Or run the full demo flow:

./scripts/run_demo.sh 200