Complying with the Law with F# and Event Sourcing

12/23/2025

by Pedro León

This article is part of the FsAdvent 2025.
Thanks to Sergey Tihon for this wonderful initiative for the community.

Strings Digital Products
We are a software development studio with over 20 years of professional experience based in Madrid, specializing in critical
systems, event‑driven architectures, and domain‑driven design.
We work with clients from anywhere in the world, building robust, maintainable digital products that are designed to last.

You can read the spanish version of this article here

The Origin

In 2021 a law was passed in Spain that directly affects software developers who build invoicing systems.
For the first time in the country’s history the government regulated how a program must behave at a technical level, requiring
guarantees for invoice issuance through a law and its corresponding
Regulation.

Failing to comply with the technical regulation carries fines between €50,000 and €150,000 for software vendors.
For the first time a design flaw or a poor implementation could translate into a penalty of hundreds of thousands of euros.

Choosing Technology to Comply with the Law

Given this scenario we decided to be very conservative.
Better to go slow than to crash.

From the outset we made a key decision:

We would represent the legal requirements in such a way that we could compile them.

The F# compiler would be our ally.
If something didn’t compile, it couldn’t reach production.
If it didn’t reach production, it couldn’t generate an illegal invoice.

To achieve this we used two well‑known tools in this community:

  • We modeled each workflow using types, guaranteeing that it would be impossible to connect two steps incorrectly.
    We put special emphasis on making incorrect states unrepresentable, following the principle of
    “making illegal states unrepresentable” (Scott Wlaschin).

  • We adopted Event Sourcing as an architectural pattern.
    Our use case fits this approach particularly well: simply by using Event Sourcing we automatically satisfy three key legal
    requirements: integrity, traceability, and immutability of business documents.

    For this we used Equinox and Propulsion on top of

MessageDB.

Modeling the Invoice Issuance Workflow

Our service contains dozens of modeled workflows.
For this article we focus on one that is especially relevant from a legal standpoint:
the invoice issuance workflow.

Issuing an invoice involves generating an invoice from a draft invoice and a billing series.

The draft is the business document the user works on: they edit items, prices, recipient data, etc.
When they consider the draft correct, they can issue an invoice, which from that point must be immutable.

The invoice needs a number with very strict legal implications: it must be consecutive, coherent with the date, and unique.
There can be no gaps or duplicates, nor two invoices derived from the same draft.

Issuing an invoice involves three distinct aggregates:

  • Draft: the mutable prior business document.
  • Serie: responsible for assigning consecutive invoice numbers.
  • Invoice: the legal immutable invoice, identified by an InvoiceId.

Moreover, the three aggregates must change their internal state coherently:

  • The Draft must not allow more than one invoice to be issued from the same draft.
  • The Serie must issue exactly the number that corresponds.
  • The Invoice cannot be created twice with the same InvoiceId.

Equinox guarantees transactionality at the aggregate level, but not across multiple aggregates simultaneously. Yet the process had
to be atomic from the domain’s perspective.

Because we couldn’t naturally use a database‑level transaction, we decided that the best approach was to model the transaction at the
domain level
.

How We Made a Process Transactional Without Database Transactions

We have three aggregates in our Issuance process, and all three will receive events if the process succeeds correctly.
Just like a database transaction has a BEGIN and ends with a COMMIT or ROLLBACK, we do the same at the aggregate level.

The natural aggregate to perform this process is the Draft itself. We must ensure that when issuing an invoice from the draft it
can’t be started more than once.

If we looked at this in high‑level pseudocode, it would look something like this (the real implementation is more complex):

async {

    // BEGIN
    // Only the first process that invokes this line gets to proceed.
    let! draftInIssuanceProgress : DraftReadModel.IssuanceInProgress =
        draftId
        |> DraftService.tryStartIssuance

    try

        // If the transaction has been started, the following commands will always succeed
        // by design unless an exception occurs.
        let! invoiceId =
            SerieService.issueNextNumber  (draftId, draftInIssuanceProgress)

        let! issuedInvoice =
            InvoiceService.issue invoiceId draftInIssuanceProgress

        do! IssuanceInProgress =
            DraftService.commitIssuance draftId invoiceId

        return invoiceId, issuedInvoice
    with
    | ex ->
        Logger.fatal "...." ex
        DraftService.rollbackIssuance draftId ex

        ....
}

Our pseudocode shows a simulated application‑level transaction that works fine in principle, but there is an important detail that any
experienced programmer would have noticed.
It’s not a real transaction, and there is a subtle trap waiting to surface.

The trap, not obvious, waiting to appear at the most unexpected moment, is an error when attempting to do rollbackIssuance that will
leave the Draft aggregate in a state of started transaction forever.

We solved this with an external process using the Automation pattern and carefully tuning the timeout parameters of the
connection to our database:

  • On the one hand, in our Postgres connectionString we set timeout parameters such as Timeout=1; Command Timeout=1; Cancellation Timeout=1 which indicates that we wait 1 second to establish a connection or execute a command or read a response when a query is
    cancelled or times out.

  • On the other hand we have an external process that follows the Automation
    Pattern
    and that has its own connection pool. If the process detects that
    an aggregate has been in the started‑transaction state for more than 10.0 seconds, it rolls back the aggregate.

The combination of these times gives us confidence: after 10.0 seconds without changing the state it means that any execution of the
workflow has thrown a timeout exception with the database.

How We Modeled the Draft Aggregate to Behave Transactionally

After looking at the pseudocode of the process, let’s move to how we implemented it in an aggregate.
For this we modeled three new events that didn’t exist in the aggregate until that point:

  • IssuanceStarted marks the start of the transaction in the domain. Think of it as BEGIN in database transactions.
    This event can only be generated from the StartIssuance command.
    Once this event is added to the aggregate’s stream, the state changes from Open to IssuanceInProgress.
    This command can produce three possible results when invoking the aggregate’s decide function (see
    Decider):

    • Ok [IssuanceStarted], which only occurs when the aggregate is in the Open state.
    • Error IssuanceIsAlreadyInProgress, which occurs when the draft is in the IssuanceInProgress state and indicates that the

transaction has already started and another one should not be started.

  • Error IssuanceIsAlreadyCommitted, which occurs when the draft is in the IssuanceCommitted state and indicates that this draft
    has already generated an invoice and therefore cannot be issued again.

  • IssuanceCommitted is the aggregate Draft event that reflects that the invoice issuance process has successfully completed.
    Once this event is added to the aggregate’s stream, its internal state changes to IssuanceCommitted, and from that point the
    aggregate accepts no further events.
    Only the CommitIssuance command can bring the aggregate to this state.
    This command can produce three possible results when invoking the aggregate’s decide function:

    • Ok [IssuanceCommitted {InvoiceId: InvoiceId}], indicating that the process has succeeded and storing the issued invoice

identifier (which helps us generate linking functionality in future projections).

  • Error IssuanceNotStarted, indicating that the aggregate did not start a transaction for invoice issuance.

  • Error IssuanceAlreadyCommitted, indicating that the aggregate already generated an invoice previously.

  • Finally, the IssuanceRolledBack event is the aggregate Draft event that reflects that the issuance process failed for some
    reason (bug, connection error with the other aggregates’ databases, or any other reason).
    Once this event is added to the stream, the aggregate returns to the Open state (allowing the transaction to be restarted).
    Only the RollbackIssuance command can bring the aggregate to this state.
    This command can produce three possible results when invoking the aggregate’s decide function:

    • Ok [IssuanceRolledBack {Error: IssuanceError}], indicating that the process failed and storing the error for monitoring and audit

purposes.

  • Error IssuanceNotStarted, indicating that the aggregate did not start a transaction for invoice issuance and therefore cannot be
    rolled back.
  • Error IssuanceAlreadyCommitted, indicating that the aggregate had already generated an invoice previously and therefore does not
    allow rollback.

All of the above can be seen in this diagram where the state transitions are the events labeled on the arrows and the internal state of
the Draft aggregate is shown in each box.

Draft state machine diagram

Modeling the Workflow with Types

Given all that, we move on to modeling the workflow.
By designing the signatures of the dependencies with types, we make ourselves safer, preventing unintended mistakes by forcing the
correct order through the types.

Our workflow’s signature is:

type TryIssueWorkflow =
    CurrentDate
    -> TryBeginIssuanceWorkflow
    -> AssignNumberWorkflow
    -> IssueInvoiceWorkflow
    -> TryCommitIssuanceWorkflow
    -> TryRollbackIssuanceWorkflow
    -> DraftId
    -> SerieId
    -> Async<Result<InvoiceId * ReadModel.Issued, ProblemWith>>

TryBeginIssuanceWorkflow has this shape:

type TryBeginIssuanceWorkflow =
    DraftId
    -> DocumentSerieId
    -> DateOnly
    -> Async<Result<DraftReadModel.IssuanceInProgress, ProblemWith>>

If we look at the types we see that, in the correct case, it returns a DraftReadModel.IssuanceInProgress. This read model contains
the state change we discussed earlier. If the method isn’t called, the returned read model will not be in this state.

Next is AssignNumberWorkflow, a command that receives a Serie. It defines a clear precondition: it requires a
DraftReadModel.IssuanceInProgress (which is only obtained after starting the previous transaction) to be able to perform this step.
No data from the read model is stored, but it is requested as a parameter so that the sub‑workflows cannot be called in a disordered
way.

type AssignNumberWorkflow =
    DocumentSerieId
    -> DraftReadModel.IssuanceInProgress
    -> Async<InvoiceId>

IssueInvoiceWorkflow will emit the invoice from an InvoiceId (which could only be generated in the previous step by the Serie
aggregate) and needs the DraftReadModel.IssuanceInProgress because it copies all the business document data.

type IssueInvoiceWorkflow = InvoiceId -> DraftReadModel.IssuanceInProgress -> Async<ReadModel.Issued>

CurrentDate simply returns the official date of the Iberian Peninsula when the invoice is issued. It is effectively a piece of data
with legal implications.

type CurrentDate =
    unit -> DateOnly

Both TryCommitIssuanceWorkflow and TryRollbackIssuanceWorkflow we already know well, but we include them here to show that they
also request the DraftReadModel.IssuanceInProgress, making them callable only within a transaction. No read‑model data is stored in
this case either.

type TryCommitIssuanceWorkflow =
    (DraftId * DraftReadModel.IssuanceInProgress)
    -> InvoiceId
    -> DateTimeOffset
    -> Async<Result<DraftReadModel.Issued, ProblemWith>>
type TryRollbackIssuanceWorkflow =
    DraftRollbackError
    -> (DraftId * DraftReadModel.IssuanceInProgress)
    -> Async<Result<DraftReadModel.Open, ProblemWith>>

With all of this we can easily compose a high‑level workflow from its dependencies, which are simply simpler workflows. In
practice, these workflows are materialized as calls to the public methods exposed by each aggregate.

In our case we follow the Service pattern per aggregate, as proposed by the Equinox Programming
Model
.

These services are resolved via dependency injection in ASP.NET Core, which keeps the endpoint handlers clean, declarative, and
expressive at the same time.

We do not include the controller code in this article because it would unnecessarily lengthen the content. We’ll leave it as material
for a future post.

Conclusion

F# allowed us to turn legal requirements into compile‑time types, and that difference was decisive.
When an error can become a real monetary penalty, confidence in the design moves from a luxury to a necessity.

Many of the ideas I applied here are not new or original.
The emphasis on the domain, on making illegal states unrepresentable, and on explicit workflow modeling is deeply influenced by the
work of Scott Wlaschin, especially in Domain‑Driven Design Made Functional.
Likewise, the way we reason about system behavior through events, and separate decision from state evolution, directly draws from
Jérémie Chassaing’s work on Event Sourcing and the Decider pattern.

None of this would have been practical without tools that make it viable in real systems.
In our case, Equinox (and Propulsion) with MessageDb (thanks to Einar Norðfjörð) gave us the scaffolding needed to bring these
ideas into production safely, explicitly, and maintainably. My sincere thanks to their creators for proving that Event Sourcing in F#
is not just elegant, but industrial‑grade.

Sincerely, without a language like F#, with such an expressive type system and a semantics so aligned with the domain, I would have had
far less confidence implementing such sensitive legal requirements.

To the F# community: thank you for sharing knowledge, patterns, and real‑world examples.
This article is, in large part, a direct result of learning from you.

In a regulated system, that’s not just a technical decision.
It’s a way to sleep peacefully… and keep trusting this language and this community.