Try formal verification

[chfast]

For formal verification is it suggested to try https://github.com/ethereum/oyente.

[mfranciszkiewicz]

I don't think this tool is reliable enough. Initial result:

Contract GolemNetworkToken:
Running, please wait...
[...]
    ============ Results ===========
      CallStack Attack:      False
[...]
      Concurrency Bug:   False
      Time Dependency:   False
      Reentrancy bug exists: True
    ====== Analysis Completed ======

After replacing

contract GolemNetworkToken {
    string public constant name = "Golem Network Token";

with

contract GolemNetworkToken {
    string constant name = "Golem Network Token";

The reentrancy bug is no longer.

solc: 0.4.2-develop.2016.9.17+commit.af6afb04.Linux.g++
oyente: 43a1755
z3: z3-4.4.1

[chfast]

public generates additional getter function name().

We may ask questions about the results in https://gitter.im/ethereum/formal-methods.