Does any SQL engine have navigation support in CHECK clauses? Imagine a simple database to track personal spending. The most basic form of the model should let you create any number of accounts and any number of transactions (specifying the spending amount, date and associated account). 

Also, some transactions may be part of a transfer between different accounts and not a legitimate expense/income on its own (for instance a money cash out from your checking account), these should be linked together somehow. I could start modelling the application with the following schema:

CREATE TABLE accounts (
  id SERIAL PRIMARY KEY
);

CREATE TABLE transactions (
  id SERIAL PRIMARY KEY,
  amount INT NOT NULL,
  date DATE NOT NULL,
  account INT NOT NULL REFERENCES accounts
);

CREATE TABLE transfers (
  outgoing_tx INT REFERENCES transactions,
  incoming_tx INT REFERENCES transactions,
  PRIMARY KEY (outgoing_tx, incoming_tx)
);


Now comes the question part. When I find myself modelling a domain like this I tend to heavily rely on CHECK clauses to further constrain the schema to the domain and ban unwanted values/states at runtime.

For instance, in this example I wouldn't care for empty transactions:

ALTER TABLE transactions
ADD CONSTRAINT no_pointless_txs CHECK (amount &lt;&gt; 0);


However, when it comes to rules that involve more than a single nice little row I always feel like I need to write too much boilerplate code. For transfers you would want to check that the transactions they point to belong to different accounts, are from the same day and have the same amount, except outgoing_tx must be negative and incoming_tx positive.

This is more or less what I would like to write, i.e. I'd like to navigate through foreign keys to access other table columns by doing select/joins under the hood:

ALTER TABLE transfers
ADD CONSTRAINT no_same_accounts
  CHECK (outgoing_tx-&gt;account-&gt;id &lt;&gt; incoming_tx-&gt;account-&gt;id),

ADD CONSTRAINT no_different_dates
  CHECK (outgoing_tx-&gt;date = incoming_tx-&gt;date),

ADD CONSTRAINT correct_balance
  CHECK (outgoing_tx-&gt;amount &lt; 0 AND 0 = outgoing_tx-&gt;amount + incoming_tx-&gt;amount);


Instead, every time I want to enforce rules like these I have no option but to write lenghty boilerplate PL/SQL functions such as get_date(int) or get_account_id(int) to do the queries manually.

CREATE OR REPLACE FUNCTION get_account_id(tx_id int) RETURNS int AS $$
  SELECT account FROM transactions WHERE id = $1;
$$ LANGUAGE SQL;

-- Every other function...

ALTER TABLE transfers
ADD CONSTRAINT no_same_accounts
  CHECK (get_account_id(outgoing_tx) &lt;&gt; get_account_id(incoming_tx));

-- Every other constraint using its corresponding function...


So I guess I just want to know if there are easier, more mantainable ways to go about this kind of use case, and OCL-style navigation came to my mind.
It appears you are looking for a SQL database that implements the SQL Standard CREATE ASSERTION statement. AFAIK there is no mainstream SQL database that actually supports this.

Therefore, the more complex data integrity rules that you wish to implement must be done so programmatically. This can be done using triggers in the DBMS or procedurally either using stored procedures in the database or within the external application.

However it is implemented, careful consideration needs to be made to ensure the ACID properties are followed to ensure the reliability of the database transactions. In particular this may mean explicit locking mechanisms are employed wherever the constraints are validated.

There is generally also the requirement to ensure that the constraints are enforced as efficiently as possible.

For an in-depth examination of the implementation of complex integrity constraints using DBMS triggers I would suggest reading Applied Mathematics for Database Professionals by Lex de Haan and Toon Koppelaars.